diff --git a/thys/Forcing/Renaming_Auto.thy b/thys/Forcing/Renaming_Auto.thy
--- a/thys/Forcing/Renaming_Auto.thy
+++ b/thys/Forcing/Renaming_Auto.thy
@@ -1,51 +1,50 @@
 theory Renaming_Auto
   imports
     Renaming
     ZF.Finite
     ZF.List
   keywords "rename" :: thy_decl % "ML"
     and "simple_rename" :: thy_decl % "ML"
     and "src"
     and "tgt"
   abbrevs "simple_rename" = ""
 begin
 
 lemmas app_fun = apply_iff[THEN iffD1]
 lemmas nat_succI = nat_succ_iff[THEN iffD2]
-ML_file\<open>Utils.ml\<close>
-ML_file\<open>Renaming_ML.ml\<close>
+ML_file \<open>utils.ML\<close>
+ML_file \<open>renaming.ML\<close>
 ML\<open>
-  open Renaming_ML
-
   fun renaming_def mk_ren name from to ctxt =
     let val to = to |> Syntax.read_term ctxt
         val from = from |> Syntax.read_term ctxt
         val (tc_lemma,action_lemma,fvs,r) = mk_ren from to ctxt
-        val (tc_lemma,action_lemma) = (fix_vars tc_lemma fvs ctxt , fix_vars action_lemma fvs ctxt)
+        val (tc_lemma,action_lemma) =
+          (Renaming.fix_vars tc_lemma fvs ctxt, Renaming.fix_vars action_lemma fvs ctxt)
         val ren_fun_name = Binding.name (name ^ "_fn")
         val ren_fun_def =  Binding.name (name ^ "_fn_def")
         val ren_thm = Binding.name (name ^ "_thm")
     in
       Local_Theory.note   ((ren_thm, []), [tc_lemma,action_lemma]) ctxt |> snd |>
       Local_Theory.define ((ren_fun_name, NoSyn), ((ren_fun_def, []), r)) |> snd      
   end;
 \<close>
 
 ML\<open>
 local
 
   val ren_parser = Parse.position (Parse.string --
       (Parse.$$$ "src" |-- Parse.string --| Parse.$$$ "tgt" -- Parse.string));
 
   val _ =
    Outer_Syntax.local_theory \<^command_keyword>\<open>rename\<close> "ML setup for synthetic definitions"
-     (ren_parser >> (fn ((name,(from,to)),_) => renaming_def sum_rename name from to ))
+     (ren_parser >> (fn ((name,(from,to)),_) => renaming_def Renaming.sum_rename name from to ))
 
   val _ =
    Outer_Syntax.local_theory \<^command_keyword>\<open>simple_rename\<close> "ML setup for synthetic definitions"
-     (ren_parser >> (fn ((name,(from,to)),_) => renaming_def ren_thm name from to ))
+     (ren_parser >> (fn ((name,(from,to)),_) => renaming_def Renaming.ren_thm name from to ))
 
 in
 end
 \<close>
 end
\ No newline at end of file
diff --git a/thys/Forcing/Synthetic_Definition.thy b/thys/Forcing/Synthetic_Definition.thy
--- a/thys/Forcing/Synthetic_Definition.thy
+++ b/thys/Forcing/Synthetic_Definition.thy
@@ -1,128 +1,128 @@
 section\<open>Automatic synthesis of formulas\<close>
 
 theory Synthetic_Definition
   imports "ZF-Constructible.Formula"
   keywords "synthesize" :: thy_decl % "ML"
     and "synthesize_notc" :: thy_decl % "ML"
     and "from_schematic"
 begin
 
-ML_file\<open>Utils.ml\<close>
+ML_file \<open>utils.ML\<close>
 
 ML\<open>
 val $` = curry ((op $) o swap)
 infix $`
 
 fun pair f g x = (f x, g x)
 
 fun display kind pos (thms,thy) =
   let val _ = Proof_Display.print_results true pos thy ((kind,""),[thms])
   in thy
 end
 
 fun prove_tc_form goal thms ctxt =
   Goal.prove ctxt [] [] goal
      (fn _ => rewrite_goal_tac ctxt thms 1
               THEN TypeCheck.typecheck_tac ctxt)
 
 fun prove_sats goal thms thm_auto ctxt =
   let val ctxt' = ctxt |> Simplifier.add_simp (thm_auto |> hd)
   in
   Goal.prove ctxt [] [] goal
      (fn _ => rewrite_goal_tac ctxt thms 1
               THEN PARALLEL_ALLGOALS (asm_simp_tac ctxt')
               THEN TypeCheck.typecheck_tac ctxt')
   end
 
 fun is_mem (@{const mem} $ _ $  _) = true
   | is_mem _ = false
 
 fun synth_thm_sats def_name term lhs set env hyps vars vs pos thm_auto lthy =
 let val (_,tm,ctxt1) = Utils.thm_concl_tm lthy term
     val (thm_refs,ctxt2) = Variable.import true [Proof_Context.get_thm lthy term] ctxt1 |>> #2
     val vs' = map (Thm.term_of o #2) vs
     val vars' = map (Thm.term_of o #2) vars
     val r_tm = tm |> Utils.dest_lhs_def |> fold (op $`) vs'
     val sats = @{const apply} $ (@{const satisfies} $ set $ r_tm) $ env
     val rhs = @{const IFOL.eq(i)} $ sats $ (@{const succ} $ @{const zero})
     val concl = @{const IFOL.iff} $ lhs $ rhs
     val g_iff = Logic.list_implies(hyps, Utils.tp concl)
     val thm = prove_sats g_iff thm_refs thm_auto ctxt2
     val name = Binding.name (def_name ^ "_iff_sats")
     val thm = Utils.fix_vars thm (map (#1 o dest_Free) vars') lthy
  in
    Local_Theory.note ((name, []), [thm]) lthy |> display "theorem" pos
  end
 
 fun synth_thm_tc def_name term hyps vars pos lthy =
 let val (_,tm,ctxt1) = Utils.thm_concl_tm lthy term
     val (thm_refs,ctxt2) = Variable.import true [Proof_Context.get_thm lthy term] ctxt1
                     |>> #2
     val vars' = map (Thm.term_of o #2) vars
     val tc_attrib = @{attributes [TC]}
     val r_tm = tm |> Utils.dest_lhs_def |> fold (op $`) vars'
     val concl = @{const mem} $ r_tm $ @{const formula}
     val g = Logic.list_implies(hyps, Utils.tp concl)
     val thm = prove_tc_form g thm_refs ctxt2
     val name = Binding.name (def_name ^ "_type")
     val thm = Utils.fix_vars thm (map (#1 o dest_Free) vars') ctxt2
  in
    Local_Theory.note ((name, tc_attrib), [thm]) lthy |> display "theorem" pos
  end
 
 
 fun synthetic_def def_name thmref pos tc auto thy =
   let
     val (thm_ref,_) = thmref |>> Facts.ref_name
     val (((_,vars),thm_tms),_) = Variable.import true [Proof_Context.get_thm thy thm_ref] thy
     val (tm,hyps) = thm_tms |> hd |> pair Thm.concl_of Thm.prems_of
     val (lhs,rhs) = tm |> Utils.dest_iff_tms o Utils.dest_trueprop
     val ((set,t),env) = rhs |> Utils.dest_sats_frm
     fun olist t = Ord_List.make String.compare (Term.add_free_names t [])
     fun relevant ts (@{const mem} $ t $ _) = not (Term.is_Free t) orelse
         Ord_List.member String.compare ts (t |> Term.dest_Free |> #1)
       | relevant _ _ = false
     val t_vars = olist t
     val vs = List.filter (fn (((v,_),_),_) => Utils.inList v t_vars) vars
     val at = List.foldr (fn ((_,var),t') => lambda (Thm.term_of var) t') t vs
     val hyps' = List.filter (relevant t_vars o Utils.dest_trueprop) hyps
   in
     Local_Theory.define ((Binding.name def_name, NoSyn),
                         ((Binding.name (def_name ^ "_def"), []), at)) thy |> #2 |>
     (if tc then synth_thm_tc def_name (def_name ^ "_def") hyps' vs pos else I) |>
     (if auto then synth_thm_sats def_name (def_name ^ "_def") lhs set env hyps vars vs pos thm_tms else I)
 
 end
 \<close>
 ML\<open>
 
 local
   val synth_constdecl =
        Parse.position (Parse.string -- ((Parse.$$$ "from_schematic" |-- Parse.thm)));
 
   val _ =
      Outer_Syntax.local_theory \<^command_keyword>\<open>synthesize\<close> "ML setup for synthetic definitions"
        (synth_constdecl >> (fn ((bndg,thm),p) => synthetic_def bndg thm p true true))
 
   val _ =
      Outer_Syntax.local_theory \<^command_keyword>\<open>synthesize_notc\<close> "ML setup for synthetic definitions"
        (synth_constdecl >> (fn ((bndg,thm),p) => synthetic_def bndg thm p false false))
 
 in
 
 end
 \<close>
 text\<open>The \<^ML>\<open>synthetic_def\<close> function extracts definitions from
 schematic goals. A new definition is added to the context. \<close>
 
 (* example of use *)
 (*
 schematic_goal mem_formula_ex :
   assumes "m\<in>nat" "n\<in> nat" "env \<in> list(M)"
   shows "nth(m,env) \<in> nth(n,env) \<longleftrightarrow> sats(M,?frm,env)"
   by (insert assms ; (rule sep_rules empty_iff_sats cartprod_iff_sats | simp del:sats_cartprod_fm)+)
 
 synthesize "\<phi>" from_schematic mem_formula_ex
 *)
 
 end
diff --git a/thys/Forcing/Renaming_ML.ml b/thys/Forcing/renaming.ML
rename from thys/Forcing/Renaming_ML.ml
rename to thys/Forcing/renaming.ML
--- a/thys/Forcing/Renaming_ML.ml
+++ b/thys/Forcing/renaming.ML
@@ -1,178 +1,178 @@
 (* Builds the finite mapping. *)
-structure Renaming_ML = struct
+structure Renaming = struct
 open Utils
 
 fun sum_ f g m n p = @{const Renaming.sum} $ f $ g $ m $ n $ p
 
 fun mk_ren rho rho' ctxt =
   let val rs  = to_ML_list rho
       val rs' = to_ML_list rho'
       val ixs = 0 upto (length rs-1)
       fun err t = "The element " ^ Syntax.string_of_term ctxt t ^ " is missing in the target environment"
       fun mkp i =
           case find_index (fn x => x = nth rs i) rs' of
             ~1 => nth rs i |> err |> error
           |  j => mk_Pair (mk_ZFnat i) (mk_ZFnat j) 
   in  map mkp ixs |> mk_FinSet
   end                           
 
 fun mk_dom_lemma ren rho =
   let val n = rho |> to_ML_list |> length |> mk_ZFnat
   in eq_ n (@{const domain} $ ren) |> tp
 end
 
 fun ren_tc_goal fin ren rho rho' =
   let val n = rho |> to_ML_list |> length
       val m = rho' |> to_ML_list |> length
       val fun_ty = if fin then @{const_name "FiniteFun"} else @{const_abbrev "function_space"}
       val ty = Const (fun_ty,@{typ "i \<Rightarrow> i \<Rightarrow> i"}) $ mk_ZFnat n $ mk_ZFnat m
   in  mem_ ren ty |> tp
 end
 
 fun ren_action_goal ren rho rho' ctxt =
   let val setV = Variable.variant_frees ctxt [] [("A",@{typ i})] |> hd |> Free
       val j = Variable.variant_frees ctxt [] [("j",@{typ i})] |> hd |> Free 
       val vs = rho  |> to_ML_list
       val ws = rho' |> to_ML_list |> filter isFree 
       val h1 = subset_ (vs|> mk_FinSet) setV
       val h2 = lt_ j (mk_ZFnat (length vs))
       val fvs = ([j,setV ] @ ws |> filter isFree) |> map freeName
       val lhs = nth_ j rho
       val rhs = nth_ (app_ ren j)  rho'
       val concl = eq_ lhs rhs
    in (Logic.list_implies([tp h1,tp h2],tp concl),fvs)
   end
 
   fun sum_tc_goal f m n p = 
     let val m_length = m |> to_ML_list |> length |> mk_ZFnat
         val n_length = n |> to_ML_list |> length |> mk_ZFnat
         val p_length = p |> length_
         val id_fun = @{const id} $ p_length
         val sum_fun = sum_ f id_fun m_length n_length p_length
         val dom = add_ m_length p_length
         val codom = add_ n_length p_length
         val fun_ty = @{const_abbrev "function_space"}
         val ty = Const (fun_ty,@{typ "i \<Rightarrow> i \<Rightarrow> i"}) $ dom $ codom
   in  (sum_fun, mem_ sum_fun ty |> tp)
   end
 
 fun sum_action_goal ren rho rho' ctxt =
   let val setV = Variable.variant_frees ctxt [] [("A",@{typ i})] |> hd |> Free
       val envV = Variable.variant_frees ctxt [] [("env",@{typ i})] |> hd |> Free
       val j = Variable.variant_frees ctxt [] [("j",@{typ i})] |> hd |> Free 
       val vs = rho  |> to_ML_list
       val ws = rho' |> to_ML_list |> filter isFree 
       val envL =  envV |> length_
       val rhoL = vs |> length |> mk_ZFnat
       val h1 = subset_ (append vs ws |> mk_FinSet) setV
       val h2 = lt_ j (add_ rhoL envL)
       val h3 = mem_ envV (list_ setV)
       val fvs = ([j,setV,envV] @ ws |> filter isFree) |> map freeName
       val lhs = nth_ j (concat_ rho envV)
       val rhs = nth_ (app_ ren j) (concat_ rho' envV)
       val concl = eq_ lhs rhs
    in (Logic.list_implies([tp h1,tp h2,tp h3],tp concl),fvs)
   end
 
   (* Tactics *)
   fun fin ctxt = 
          REPEAT (resolve_tac ctxt [@{thm nat_succI}] 1)
          THEN   resolve_tac ctxt [@{thm nat_0I}] 1
 
   fun step ctxt thm = 
     asm_full_simp_tac ctxt 1
     THEN asm_full_simp_tac ctxt 1
     THEN EqSubst.eqsubst_tac ctxt [1] [@{thm app_fun} OF [thm]] 1
     THEN simp_tac ctxt 1
     THEN simp_tac ctxt 1
 
   fun fin_fun_tac ctxt = 
     REPEAT (
       resolve_tac ctxt [@{thm consI}] 1
       THEN resolve_tac ctxt [@{thm ltD}] 1
       THEN simp_tac ctxt 1
       THEN resolve_tac ctxt [@{thm ltD}] 1
       THEN simp_tac ctxt 1)
     THEN resolve_tac ctxt [@{thm emptyI}] 1
   THEN REPEAT (simp_tac ctxt 1)
 
   fun ren_thm e e' ctxt = 
    let
     val r = mk_ren e e' ctxt
     val fin_tc_goal = ren_tc_goal true r e e' 
     val dom_goal =  mk_dom_lemma r e
     val tc_goal = ren_tc_goal false r e e'
     val (action_goal,fvs) = ren_action_goal r e e' ctxt
     val fin_tc_lemma = Goal.prove ctxt [] [] fin_tc_goal (fn _ => fin_fun_tac ctxt)
     val dom_lemma = Goal.prove ctxt [] [] dom_goal (fn _ => blast_tac ctxt 1) 
     val tc_lemma =  Goal.prove ctxt [] [] tc_goal
             (fn _ =>  EqSubst.eqsubst_tac ctxt [1] [dom_lemma] 1
               THEN resolve_tac ctxt [@{thm FiniteFun_is_fun}] 1
               THEN resolve_tac ctxt [fin_tc_lemma] 1)
     val action_lemma = Goal.prove ctxt [] [] action_goal
               (fn _ => 
                   forward_tac ctxt [@{thm le_natI}] 1
                   THEN fin ctxt
                   THEN REPEAT (resolve_tac ctxt [@{thm natE}] 1
                                THEN step ctxt tc_lemma)
                   THEN (step ctxt tc_lemma)
               )
     in (action_lemma, tc_lemma, fvs, r)
   end
 
 (* 
 Returns the sum renaming, the goal for type_checking, and the actual lemmas 
 for the left part of the sum.
 *)
  fun sum_ren_aux e e' ctxt = 
   let val env = Variable.variant_frees ctxt [] [("env",@{typ i})] |> hd |> Free
       val (left_action_lemma,left_tc_lemma,_,r) = ren_thm e e' ctxt
       val (sum_ren,sum_goal_tc) = sum_tc_goal r e e' env
       val setV = Variable.variant_frees ctxt [] [("A",@{typ i})] |> hd |> Free      
       fun hyp en = mem_ en (list_ setV)
   in (sum_ren,
       freeName env,
       Logic.list_implies (map (fn e => e |> hyp |> tp) [env], sum_goal_tc),
       left_tc_lemma,
       left_action_lemma)
 end
 
 fun sum_tc_lemma rho rho' ctxt =
   let val (sum_ren, envVar, tc_goal, left_tc_lemma, left_action_lemma) = sum_ren_aux rho rho' ctxt
       val (goal,fvs) = sum_action_goal sum_ren rho rho' ctxt
       val r = mk_ren rho rho' ctxt
   in (sum_ren, goal,envVar, r,left_tc_lemma, left_action_lemma ,fvs, Goal.prove ctxt [] [] tc_goal
                (fn _ =>
             resolve_tac ctxt [@{thm sum_type_id_aux2}] 1
             THEN asm_simp_tac ctxt 4
             THEN simp_tac ctxt 1
             THEN resolve_tac ctxt [left_tc_lemma] 1            
             THEN (fin ctxt)
             THEN (fin ctxt)
   ))
   end
 
 fun sum_rename rho rho' ctxt = 
   let
     val (_, goal, _, left_rename, left_tc_lemma, left_action_lemma, fvs, sum_tc_lemma) = sum_tc_lemma rho rho' ctxt
     val action_lemma = fix_vars left_action_lemma fvs ctxt
   in (sum_tc_lemma, Goal.prove ctxt [] [] goal
     (fn _ => resolve_tac ctxt [@{thm sum_action_id_aux}] 1
             THEN (simp_tac ctxt 4)
             THEN (simp_tac ctxt 1)
             THEN (resolve_tac ctxt [left_tc_lemma]  1)
             THEN (asm_full_simp_tac ctxt 1) 
             THEN (asm_full_simp_tac ctxt 1)
             THEN (simp_tac ctxt 1)
             THEN (simp_tac ctxt 1)
             THEN (simp_tac ctxt 1)
             THEN (full_simp_tac ctxt 1)
             THEN (resolve_tac ctxt [action_lemma] 1)
             THEN (blast_tac ctxt  1)
             THEN (full_simp_tac ctxt  1)
             THEN (full_simp_tac ctxt  1)
     
    ), fvs, left_rename
    )
 end ;
 end
\ No newline at end of file
diff --git a/thys/Forcing/Utils.ml b/thys/Forcing/utils.ML
rename from thys/Forcing/Utils.ml
rename to thys/Forcing/utils.ML
--- a/thys/Forcing/Utils.ml
+++ b/thys/Forcing/utils.ML
@@ -1,126 +1,126 @@
-signature Utils =
+signature UTILS =
  sig
     val binop : term -> term -> term -> term
     val add_: term -> term -> term
     val app_: term -> term -> term
     val concat_: term -> term -> term
     val dest_apply: term -> term * term
     val dest_iff_lhs: term -> term
     val dest_iff_rhs: term -> term
     val dest_iff_tms: term -> term * term
     val dest_lhs_def: term -> term
     val dest_rhs_def: term -> term
     val dest_satisfies_tms: term -> term * term
     val dest_satisfies_frm: term -> term
     val dest_eq_tms: term -> term * term
     val dest_sats_frm: term -> (term * term) * term
     val dest_trueprop: term -> term
     val eq_: term -> term -> term
     val fix_vars: thm -> string list -> Proof.context -> thm
     val formula_: term
     val freeName: term -> string
     val inList: ''a -> ''a list -> bool
     val isFree: term -> bool
     val length_: term -> term
     val list_: term -> term
     val lt_: term -> term -> term
     val mem_: term -> term -> term
     val mk_FinSet: term list -> term
     val mk_Pair: term -> term -> term
     val mk_ZFlist: ('a -> term) -> 'a list -> term
     val mk_ZFnat: int -> term
     val nat_: term
     val nth_: term -> term -> term
     val subset_: term -> term -> term
     val thm_concl_tm :  Proof.context -> xstring -> 
         ((indexname * typ) * cterm) list * term * Proof.context
     val to_ML_list: term -> term list
     val tp: term -> term
   end
 
-structure Utils : Utils =
+structure Utils : UTILS =
 struct 
 (* Smart constructors for ZF-terms *)
 
 fun inList a = exists (fn b => a = b)
 
 fun binop h t u = h $ t $ u
 val mk_Pair  = binop @{const Pair}
 
 fun mk_FinSet nil = @{const zero}
   | mk_FinSet (e :: es) = @{const cons} $ e $ mk_FinSet es
 
 fun mk_ZFnat 0 = @{const zero}
   | mk_ZFnat n = @{const succ} $ mk_ZFnat (n-1)
 
 fun mk_ZFlist _ nil = @{const "Nil"}
   | mk_ZFlist f (t :: ts) = @{const "Cons"} $ f t $ mk_ZFlist f ts
 
 fun to_ML_list (@{const Nil}) = nil
   | to_ML_list (@{const Cons} $ t $ ts) = t :: to_ML_list ts
 |   to_ML_list _ = nil
 
 fun isFree (Free (_,_)) = true
   | isFree _ = false
 
 fun freeName (Free (n,_)) = n
   | freeName _ = error "Not a free variable"
 
 val app_ = binop @{const apply}
 
 fun tp x = @{const Trueprop} $ x
 fun length_ env = @{const length} $ env
 val nth_ = binop @{const nth}
 val add_ = binop @{const add}
 val mem_ = binop @{const mem}
 val subset_ = binop @{const Subset}
 val lt_ = binop @{const lt}
 val concat_ = binop @{const app}
 val eq_ = binop @{const IFOL.eq(i)}
 
 (* Abbreviation for sets *)
 fun list_ set = @{const list} $ set
 val nat_ = @{const nat}
 val formula_ = @{const formula}
 
 (** Destructors of terms **)
 fun dest_eq_tms (Const (@{const_name IFOL.eq},_) $ t $ u) = (t, u)
   | dest_eq_tms t = raise TERM ("dest_eq_tms", [t])
 
 fun dest_lhs_def (Const (@{const_name Pure.eq},_) $ x $ _) = x
   | dest_lhs_def t = raise TERM ("dest_lhs_def", [t])
 
 fun dest_rhs_def (Const (@{const_name Pure.eq},_) $ _ $ y) = y
   | dest_rhs_def t = raise TERM ("dest_rhs_def", [t])
 
 
 fun dest_apply (@{const apply} $ t $ u) = (t,u)
   | dest_apply t = raise TERM ("dest_applies_op", [t])
 
 fun dest_satisfies_tms (@{const Formula.satisfies} $ A $ f) = (A,f)
   | dest_satisfies_tms t = raise TERM ("dest_satisfies_tms", [t]);
 
 val dest_satisfies_frm = #2 o dest_satisfies_tms
 
 fun dest_sats_frm t = t |> dest_eq_tms |> #1 |> dest_apply |>> dest_satisfies_tms ;
 
 fun dest_trueprop (@{const IFOL.Trueprop} $ t) = t
   | dest_trueprop t = t
 
 fun dest_iff_tms (@{const IFOL.iff} $ t $ u) = (t, u)
   | dest_iff_tms t = raise TERM ("dest_iff_tms", [t])
 
 val dest_iff_lhs = #1 o dest_iff_tms
 val dest_iff_rhs = #2 o dest_iff_tms
 
 fun thm_concl_tm ctxt thm_ref =
   let val (((_,vars),thm_tms),ctxt1) = Variable.import true [Proof_Context.get_thm ctxt thm_ref] ctxt
   in (vars, thm_tms |> hd |> Thm.concl_of, ctxt1)
 end
 
 fun fix_vars thm vars ctxt = let
   val (_, ctxt1) = Variable.add_fixes vars ctxt
   in singleton (Proof_Context.export ctxt1 ctxt) thm
 end
 
 end ;