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,126 +1,129 @@
 section\<open>Automatic synthesis of formulas\<close>
 
 theory Synthetic_Definition
   imports Utils
   keywords "synthesize" :: thy_decl % "ML"
     and "synthesize_notc" :: thy_decl % "ML"
     and "from_schematic"
 begin
 
 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 thm = Proof_Context.get_thm thy thm_ref;
+    val thm_vars = rev (Term.add_vars (Thm.full_prop_of thm) []);
+    val (((_,inst),thm_tms),_) = Variable.import true [thm] thy
+    val vars = map (fn v => (v, the (Term_Subst.Vars.lookup inst v))) thm_vars;
     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/utils.ML b/thys/Forcing/utils.ML
--- a/thys/Forcing/utils.ML
+++ b/thys/Forcing/utils.ML
@@ -1,126 +1,127 @@
 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
+        cterm Term_Subst.Vars.table * term * Proof.context
     val to_ML_list: term -> term list
     val tp: term -> term
   end
 
 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
+  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 ;