--- a/src/HOL/Library/reflection.ML Sat Mar 06 19:17:59 2010 +0000
+++ b/src/HOL/Library/reflection.ML Sun Mar 07 11:57:16 2010 +0100
@@ -62,7 +62,7 @@
fun tryext x = (x RS ext2 handle THM _ => x)
val cong = (Goal.prove ctxt'' [] (map mk_def env)
(HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
- (fn x => LocalDefs.unfold_tac (#context x) (map tryext (#prems x))
+ (fn x => Local_Defs.unfold_tac (#context x) (map tryext (#prems x))
THEN rtac th' 1)) RS sym
val (cong' :: vars') =
--- a/src/HOL/NSA/transfer.ML Sat Mar 06 19:17:59 2010 +0000
+++ b/src/HOL/NSA/transfer.ML Sun Mar 07 11:57:16 2010 +0100
@@ -56,7 +56,7 @@
let
val thy = ProofContext.theory_of ctxt;
val {intros,unfolds,refolds,consts} = TransferData.get (Context.Proof ctxt);
- val meta = LocalDefs.meta_rewrite_rule ctxt;
+ val meta = Local_Defs.meta_rewrite_rule ctxt;
val ths' = map meta ths;
val unfolds' = map meta unfolds and refolds' = map meta refolds;
val (_$_$t') = concl_of (MetaSimplifier.rewrite true unfolds' (cterm_of thy t))
--- a/src/HOL/Tools/Function/mutual.ML Sat Mar 06 19:17:59 2010 +0000
+++ b/src/HOL/Tools/Function/mutual.ML Sun Mar 07 11:57:16 2010 +0100
@@ -190,7 +190,7 @@
in
Goal.prove ctxt [] []
(HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
- (fn _ => (LocalDefs.unfold_tac ctxt all_orig_fdefs)
+ (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs)
THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
THEN (simp_tac (simpset_of ctxt addsimps SumTree.proj_in_rules)) 1)
|> restore_cond
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Sat Mar 06 19:17:59 2010 +0000
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Sun Mar 07 11:57:16 2010 +0100
@@ -123,7 +123,7 @@
(* General reduction pair application *)
fun rem_inv_img ctxt =
let
- val unfold_tac = LocalDefs.unfold_tac ctxt
+ val unfold_tac = Local_Defs.unfold_tac ctxt
in
rtac @{thm subsetI} 1
THEN etac @{thm CollectE} 1
@@ -259,7 +259,7 @@
THEN mset_pwleq_tac 1
THEN EVERY (map2 (less_proof false) qs ps)
THEN (if strict orelse qs <> lq
- then LocalDefs.unfold_tac ctxt set_of_simps
+ then Local_Defs.unfold_tac ctxt set_of_simps
THEN steps_tac MAX true
(subtract (op =) qs lq) (subtract (op =) ps lp)
else all_tac)
@@ -290,7 +290,7 @@
THEN (rtac (order_rpair ms_rp label) 1)
THEN PRIMITIVE (instantiate' [] [SOME level_mapping])
THEN unfold_tac @{thms rp_inv_image_def} (simpset_of ctxt)
- THEN LocalDefs.unfold_tac ctxt
+ THEN Local_Defs.unfold_tac ctxt
(@{thms split_conv} @ @{thms fst_conv} @ @{thms snd_conv})
THEN REPEAT (SOMEGOAL (resolve_tac [@{thm Un_least}, @{thm empty_subsetI}]))
THEN EVERY (map (prove_lev true) sl)
--- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Sat Mar 06 19:17:59 2010 +0000
+++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Sun Mar 07 11:57:16 2010 +0100
@@ -127,7 +127,7 @@
check_rules fieldN f_rules 2 andalso
check_rules idomN idom 2;
- val mk_meta = LocalDefs.meta_rewrite_rule ctxt;
+ val mk_meta = Local_Defs.meta_rewrite_rule ctxt;
val sr_rules' = map mk_meta sr_rules;
val r_rules' = map mk_meta r_rules;
val f_rules' = map mk_meta f_rules;
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sat Mar 06 19:17:59 2010 +0000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sun Mar 07 11:57:16 2010 +0100
@@ -418,7 +418,7 @@
*)
fun prepare_split_thm ctxt split_thm =
(split_thm RS @{thm iffD2})
- |> LocalDefs.unfold ctxt [@{thm atomize_conjL[symmetric]},
+ |> Local_Defs.unfold ctxt [@{thm atomize_conjL[symmetric]},
@{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}]
fun find_split_thm thy (Const (name, typ)) =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sat Mar 06 19:17:59 2010 +0000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sun Mar 07 11:57:16 2010 +0100
@@ -145,7 +145,7 @@
val t' = Pattern.rewrite_term thy rewr [] t
val tac = Skip_Proof.cheat_tac thy
val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn _ => tac)
- val th''' = LocalDefs.unfold ctxt [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}] th''
+ val th''' = Local_Defs.unfold ctxt [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}] th''
in
th'''
end;
--- a/src/HOL/Tools/Quotient/quotient_def.ML Sat Mar 06 19:17:59 2010 +0000
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Sun Mar 07 11:57:16 2010 +0100
@@ -63,7 +63,7 @@
val qconst_bname = Binding.name lhs_str
val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
- val (_, prop') = LocalDefs.cert_def lthy prop
+ val (_, prop') = Local_Defs.cert_def lthy prop
val (_, newrhs) = Primitive_Defs.abs_def prop'
val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy
--- a/src/HOL/Tools/inductive.ML Sat Mar 06 19:17:59 2010 +0000
+++ b/src/HOL/Tools/inductive.ML Sun Mar 07 11:57:16 2010 +0100
@@ -832,7 +832,7 @@
let
val _ = Binding.is_empty name andalso null atts orelse
error "Abbreviations may not have names or attributes";
- val ((x, T), rhs) = LocalDefs.abs_def (snd (LocalDefs.cert_def ctxt1 t));
+ val ((x, T), rhs) = Local_Defs.abs_def (snd (Local_Defs.cert_def ctxt1 t));
val var =
(case find_first (fn ((c, _), _) => Binding.name_of c = x) cnames_syn of
NONE => error ("Undeclared head of abbreviation " ^ quote x)
@@ -854,8 +854,8 @@
val ps = map Free pnames;
val (_, ctxt2) = lthy |> Variable.add_fixes (map (Binding.name_of o fst o fst) cnames_syn');
- val _ = map (fn abbr => LocalDefs.fixed_abbrev abbr ctxt2) abbrevs;
- val ctxt3 = ctxt2 |> fold (snd oo LocalDefs.fixed_abbrev) abbrevs;
+ val _ = map (fn abbr => Local_Defs.fixed_abbrev abbr ctxt2) abbrevs;
+ val ctxt3 = ctxt2 |> fold (snd oo Local_Defs.fixed_abbrev) abbrevs;
val expand = Assumption.export_term ctxt3 lthy #> ProofContext.cert_term lthy;
fun close_rule r = list_all_free (rev (fold_aterms
--- a/src/HOL/Tools/res_axioms.ML Sat Mar 06 19:17:59 2010 +0000
+++ b/src/HOL/Tools/res_axioms.ML Sun Mar 07 11:57:16 2010 +0100
@@ -475,7 +475,7 @@
(map Thm.term_of hyps)
val fixed = OldTerm.term_frees (concl_of st) @
fold (union (op aconv)) (map OldTerm.term_frees remaining_hyps) []
- in Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
+ in Seq.of_list [Local_Defs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
fun meson_general_tac ctxt ths i st0 =
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Sat Mar 06 19:17:59 2010 +0000
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Sun Mar 07 11:57:16 2010 +0100
@@ -174,7 +174,7 @@
(K (beta_tac 1));
val tuple_unfold_thm =
(@{thm def_cont_fix_eq} OF [tuple_fixdef_thm, cont_thm])
- |> LocalDefs.unfold (ProofContext.init thy) @{thms split_conv};
+ |> Local_Defs.unfold (ProofContext.init thy) @{thms split_conv};
fun mk_unfold_thms [] thm = []
| mk_unfold_thms (n::[]) thm = [(n, thm)]
--- a/src/HOLCF/Tools/fixrec.ML Sat Mar 06 19:17:59 2010 +0000
+++ b/src/HOLCF/Tools/fixrec.ML Sun Mar 07 11:57:16 2010 +0100
@@ -146,9 +146,9 @@
val predicate = lambda_tuple lhss (list_comb (P, lhss));
val tuple_induct_thm = (def_cont_fix_ind OF [tuple_fixdef_thm, cont_thm])
|> Drule.instantiate' [] [SOME (Thm.cterm_of thy predicate)]
- |> LocalDefs.unfold lthy @{thms split_paired_all split_conv split_strict};
+ |> Local_Defs.unfold lthy @{thms split_paired_all split_conv split_strict};
val tuple_unfold_thm = (def_cont_fix_eq OF [tuple_fixdef_thm, cont_thm])
- |> LocalDefs.unfold lthy' @{thms split_conv};
+ |> Local_Defs.unfold lthy' @{thms split_conv};
fun unfolds [] thm = []
| unfolds (n::[]) thm = [(n, thm)]
| unfolds (n::ns) thm = let
--- a/src/Pure/Isar/attrib.ML Sat Mar 06 19:17:59 2010 +0000
+++ b/src/Pure/Isar/attrib.ML Sun Mar 07 11:57:16 2010 +0100
@@ -245,8 +245,8 @@
fun unfolded_syntax rule =
thms >> (fn ths => Thm.rule_attribute (fn context => rule (Context.proof_of context) ths));
-val unfolded = unfolded_syntax LocalDefs.unfold;
-val folded = unfolded_syntax LocalDefs.fold;
+val unfolded = unfolded_syntax Local_Defs.unfold;
+val folded = unfolded_syntax Local_Defs.fold;
(* rule format *)
@@ -311,7 +311,7 @@
setup (Binding.name "rulify") (Scan.succeed ObjectLogic.declare_rulify)
"declaration of rulify rule" #>
setup (Binding.name "rotated") (Scan.lift rotated) "rotated theorem premises" #>
- setup (Binding.name "defn") (add_del LocalDefs.defn_add LocalDefs.defn_del)
+ setup (Binding.name "defn") (add_del Local_Defs.defn_add Local_Defs.defn_del)
"declaration of definitional transformations" #>
setup (Binding.name "abs_def") (Scan.succeed (Thm.rule_attribute (K Drule.abs_def)))
"abstract over free variables of a definition"));
--- a/src/Pure/Isar/code.ML Sat Mar 06 19:17:59 2010 +0000
+++ b/src/Pure/Isar/code.ML Sun Mar 07 11:57:16 2010 +0100
@@ -566,7 +566,7 @@
fun assert_eqn thy = error_thm (gen_assert_eqn thy true);
-fun meta_rewrite thy = LocalDefs.meta_rewrite_rule (ProofContext.init thy);
+fun meta_rewrite thy = Local_Defs.meta_rewrite_rule (ProofContext.init thy);
fun mk_eqn thy = error_thm (gen_assert_eqn thy false) o
apfst (meta_rewrite thy);
@@ -810,7 +810,7 @@
val tyscm = typscheme_of_cert thy cert;
val thms = if null propers then [] else
cert_thm
- |> LocalDefs.expand [snd (get_head thy cert_thm)]
+ |> Local_Defs.expand [snd (get_head thy cert_thm)]
|> Thm.varifyT
|> Conjunction.elim_balanced (length propers);
in (tyscm, map (pair NONE o dest_eqn thy o Thm.prop_of) thms ~~ (map SOME thms ~~ propers)) end
--- a/src/Pure/Isar/constdefs.ML Sat Mar 06 19:17:59 2010 +0000
+++ b/src/Pure/Isar/constdefs.ML Sun Mar 07 11:57:16 2010 +0100
@@ -34,7 +34,7 @@
ProofContext.add_fixes [(x, T, mx)] #> snd #> pair (SOME x, mx)));
val prop = prep_prop var_ctxt raw_prop;
- val (c, T) = #1 (LocalDefs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
+ val (c, T) = #1 (Local_Defs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
val _ =
(case Option.map Name.of_binding d of
NONE => ()
--- a/src/Pure/Isar/element.ML Sat Mar 06 19:17:59 2010 +0000
+++ b/src/Pure/Isar/element.ML Sun Mar 07 11:57:16 2010 +0100
@@ -499,11 +499,11 @@
let
val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
- let val ((c, _), t') = LocalDefs.cert_def ctxt t (* FIXME adapt ps? *)
+ let val ((c, _), t') = Local_Defs.cert_def ctxt t (* FIXME adapt ps? *)
in (t', ((Thm.def_binding_optional (Binding.name c) name, atts), [(t', ps)])) end);
val (_, ctxt') = ctxt
|> fold Variable.auto_fixes (map #1 asms)
- |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
+ |> ProofContext.add_assms_i Local_Defs.def_export (map #2 asms);
in ctxt' end)
| init (Notes (kind, facts)) = (fn context =>
let
--- a/src/Pure/Isar/expression.ML Sat Mar 06 19:17:59 2010 +0000
+++ b/src/Pure/Isar/expression.ML Sun Mar 07 11:57:16 2010 +0100
@@ -298,7 +298,7 @@
Assumes asms => Assumes (asms |> map (fn (a, propps) =>
(a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
| Defines defs => Defines (defs |> map (fn ((name, atts), (t, ps)) =>
- let val ((c, _), t') = LocalDefs.cert_def ctxt (close_frees t)
+ let val ((c, _), t') = Local_Defs.cert_def ctxt (close_frees t)
in ((Thm.def_binding_optional (Binding.name c) name, atts), (t', no_binds ps)) end))
| e => e)
end;
@@ -513,8 +513,8 @@
fun bind_def ctxt eq (xs, env, eqs) =
let
- val _ = LocalDefs.cert_def ctxt eq;
- val ((y, T), b) = LocalDefs.abs_def eq;
+ val _ = Local_Defs.cert_def ctxt eq;
+ val ((y, T), b) = Local_Defs.abs_def eq;
val b' = norm_term env b;
fun err msg = error (msg ^ ": " ^ quote y);
in
@@ -808,8 +808,8 @@
val eqns = map (Morphism.thm (export' $> export)) raw_eqns;
val eqn_attrss = map2 (fn attrs => fn eqn =>
((apsnd o map) (Attrib.attribute_i thy) attrs, [([eqn], [])])) attrss eqns;
- fun meta_rewrite thy = map (LocalDefs.meta_rewrite_rule (ProofContext.init thy) #>
- Drule.abs_def) o maps snd;
+ fun meta_rewrite thy =
+ map (Local_Defs.meta_rewrite_rule (ProofContext.init thy) #> Drule.abs_def) o maps snd;
in
thy
|> PureThy.note_thmss Thm.lemmaK eqn_attrss
--- a/src/Pure/Isar/local_defs.ML Sat Mar 06 19:17:59 2010 +0000
+++ b/src/Pure/Isar/local_defs.ML Sun Mar 07 11:57:16 2010 +0100
@@ -34,7 +34,7 @@
((string * typ) * term) * (Proof.context -> thm -> thm)
end;
-structure LocalDefs: LOCAL_DEFS =
+structure Local_Defs: LOCAL_DEFS =
struct
(** primitive definitions **)
--- a/src/Pure/Isar/method.ML Sat Mar 06 19:17:59 2010 +0000
+++ b/src/Pure/Isar/method.ML Sun Mar 07 11:57:16 2010 +0100
@@ -165,8 +165,8 @@
(* unfold/fold definitions *)
-fun unfold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (LocalDefs.unfold_tac ctxt ths));
-fun fold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (LocalDefs.fold_tac ctxt ths));
+fun unfold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (Local_Defs.unfold_tac ctxt ths));
+fun fold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (Local_Defs.fold_tac ctxt ths));
(* atomize rule statements *)
--- a/src/Pure/Isar/proof.ML Sat Mar 06 19:17:59 2010 +0000
+++ b/src/Pure/Isar/proof.ML Sun Mar 07 11:57:16 2010 +0100
@@ -599,7 +599,7 @@
|>> map (fn (x, _, mx) => (x, mx))
|-> (fn vars =>
map_context_result (prep_binds false (map swap raw_rhss))
- #-> (fn rhss => map_context_result (LocalDefs.add_defs (vars ~~ (name_atts ~~ rhss)))))
+ #-> (fn rhss => map_context_result (Local_Defs.add_defs (vars ~~ (name_atts ~~ rhss)))))
|-> (put_facts o SOME o map (#2 o #2))
end;
@@ -681,8 +681,8 @@
in (statement, [], f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end));
fun append_using _ ths using = using @ filter_out Thm.is_dummy ths;
-fun unfold_using ctxt ths = map (LocalDefs.unfold ctxt ths);
-val unfold_goals = LocalDefs.unfold_goals;
+fun unfold_using ctxt ths = map (Local_Defs.unfold ctxt ths);
+val unfold_goals = Local_Defs.unfold_goals;
in
--- a/src/Pure/Isar/specification.ML Sat Mar 06 19:17:59 2010 +0000
+++ b/src/Pure/Isar/specification.ML Sun Mar 07 11:57:16 2010 +0100
@@ -193,7 +193,7 @@
fun gen_def do_print prep (raw_var, raw_spec) lthy =
let
val (vars, [((raw_name, atts), prop)]) = fst (prep (the_list raw_var) [raw_spec] lthy);
- val (((x, T), rhs), prove) = LocalDefs.derived_def lthy true prop;
+ val (((x, T), rhs), prove) = Local_Defs.derived_def lthy true prop;
val var as (b, _) =
(case vars of
[] => (Binding.name x, NoSyn)
@@ -232,7 +232,7 @@
val ((vars, [(_, prop)]), _) =
prep (the_list raw_var) [(Attrib.empty_binding, raw_prop)]
(lthy |> ProofContext.set_mode ProofContext.mode_abbrev);
- val ((x, T), rhs) = LocalDefs.abs_def (#2 (LocalDefs.cert_def lthy prop));
+ val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy prop));
val var =
(case vars of
[] => (Binding.name x, NoSyn)
--- a/src/Pure/Isar/theory_target.ML Sat Mar 06 19:17:59 2010 +0000
+++ b/src/Pure/Isar/theory_target.ML Sun Mar 07 11:57:16 2010 +0100
@@ -121,7 +121,7 @@
(*export assumes/defines*)
val th = Goal.norm_result raw_th;
- val (defs, th') = LocalDefs.export ctxt thy_ctxt th;
+ val (defs, th') = Local_Defs.export ctxt thy_ctxt th;
val concl_conv = MetaSimplifier.rewrite true defs (Thm.cprop_of th);
val assms = map (MetaSimplifier.rewrite_rule defs o Thm.assume) (Assumption.all_assms_of ctxt);
val nprems = Thm.nprems_of th' - Thm.nprems_of th;
@@ -152,7 +152,7 @@
val result'' =
(case SINGLE (Seq.INTERVAL assm_tac 1 nprems) result' of
NONE => raise THM ("Failed to re-import result", 0, [result'])
- | SOME res => LocalDefs.trans_props ctxt [res, Thm.symmetric concl_conv])
+ | SOME res => Local_Defs.trans_props ctxt [res, Thm.symmetric concl_conv])
|> Goal.norm_result
|> PureThy.name_thm false false name;
@@ -235,7 +235,7 @@
lthy'
|> is_locale ? term_syntax ta false (locale_const ta Syntax.mode_default ((b, mx2), t))
|> is_class ? class_target ta (Class_Target.declare target ((b, mx1), t))
- |> LocalDefs.add_def ((b, NoSyn), t)
+ |> Local_Defs.add_def ((b, NoSyn), t)
end;
@@ -266,7 +266,7 @@
(Sign.add_abbrev (#1 prmode) (b, global_rhs) #-> (fn (lhs, _) =>
Sign.notation true prmode [(lhs, mx3)])))
|> ProofContext.add_abbrev PrintMode.internal (b, t) |> snd
- |> LocalDefs.fixed_abbrev ((b, NoSyn), t)
+ |> Local_Defs.fixed_abbrev ((b, NoSyn), t)
end;
@@ -279,7 +279,7 @@
val name' = Thm.def_binding_optional b name;
val (rhs', rhs_conv) =
- LocalDefs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
+ Local_Defs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
val xs = Variable.add_fixed (Local_Theory.target_of lthy) rhs' [];
val T = Term.fastype_of rhs;
@@ -296,7 +296,7 @@
if is_none (Class_Target.instantiation_param lthy b)
then Thm.add_def false false (name', Logic.mk_equals (lhs', rhs'))
else AxClass.define_overloaded name' (fst (dest_Const lhs'), rhs'));
- val def = LocalDefs.trans_terms lthy3
+ val def = Local_Defs.trans_terms lthy3
[(*c == global.c xs*) local_def,
(*global.c xs == rhs'*) global_def,
(*rhs' == rhs*) Thm.symmetric rhs_conv];
--- a/src/Tools/Code/code_preproc.ML Sat Mar 06 19:17:59 2010 +0000
+++ b/src/Tools/Code/code_preproc.ML Sun Mar 07 11:57:16 2010 +0100
@@ -87,7 +87,7 @@
fun add_unfold_post raw_thm thy =
let
- val thm = LocalDefs.meta_rewrite_rule (ProofContext.init thy) raw_thm;
+ val thm = Local_Defs.meta_rewrite_rule (ProofContext.init thy) raw_thm;
val thm_sym = Thm.symmetric thm;
in
thy |> map_pre_post (fn (pre, post) =>
--- a/src/Tools/induct.ML Sat Mar 06 19:17:59 2010 +0000
+++ b/src/Tools/induct.ML Sun Mar 07 11:57:16 2010 +0100
@@ -683,14 +683,14 @@
fun add (SOME (_, (t, true))) ctxt = ((SOME t, []), ctxt)
| add (SOME (SOME x, (t, _))) ctxt =
let val ([(lhs, (_, th))], ctxt') =
- LocalDefs.add_defs [((x, NoSyn), (Thm.empty_binding, t))] ctxt
+ Local_Defs.add_defs [((x, NoSyn), (Thm.empty_binding, t))] ctxt
in ((SOME lhs, [th]), ctxt') end
| add (SOME (NONE, (t as Free _, _))) ctxt = ((SOME t, []), ctxt)
| add (SOME (NONE, (t, _))) ctxt =
let
val ([s], _) = Name.variants ["x"] (Variable.names_of ctxt);
val ([(lhs, (_, th))], ctxt') =
- LocalDefs.add_defs [((Binding.name s, NoSyn),
+ Local_Defs.add_defs [((Binding.name s, NoSyn),
(Thm.empty_binding, t))] ctxt
in ((SOME lhs, [th]), ctxt') end
| add NONE ctxt = ((NONE, []), ctxt);