# HG changeset patch # User wenzelm # Date 1267959436 -3600 # Node ID c4e29a0bb8c1afbe3f1451dd5decde649a62729c # Parent b0de8551fadf0710d57351a556996855d6df9ab0 modernized structure Local_Defs; diff -r b0de8551fadf -r c4e29a0bb8c1 src/HOL/Library/reflection.ML --- 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') = diff -r b0de8551fadf -r c4e29a0bb8c1 src/HOL/NSA/transfer.ML --- 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)) diff -r b0de8551fadf -r c4e29a0bb8c1 src/HOL/Tools/Function/mutual.ML --- 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 diff -r b0de8551fadf -r c4e29a0bb8c1 src/HOL/Tools/Function/scnp_reconstruct.ML --- 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) diff -r b0de8551fadf -r c4e29a0bb8c1 src/HOL/Tools/Groebner_Basis/normalizer_data.ML --- 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; diff -r b0de8551fadf -r c4e29a0bb8c1 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- 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)) = diff -r b0de8551fadf -r c4e29a0bb8c1 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- 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; diff -r b0de8551fadf -r c4e29a0bb8c1 src/HOL/Tools/Quotient/quotient_def.ML --- 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 diff -r b0de8551fadf -r c4e29a0bb8c1 src/HOL/Tools/inductive.ML --- 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 diff -r b0de8551fadf -r c4e29a0bb8c1 src/HOL/Tools/res_axioms.ML --- 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 = diff -r b0de8551fadf -r c4e29a0bb8c1 src/HOLCF/Tools/Domain/domain_isomorphism.ML --- 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)] diff -r b0de8551fadf -r c4e29a0bb8c1 src/HOLCF/Tools/fixrec.ML --- 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 diff -r b0de8551fadf -r c4e29a0bb8c1 src/Pure/Isar/attrib.ML --- 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")); diff -r b0de8551fadf -r c4e29a0bb8c1 src/Pure/Isar/code.ML --- 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 diff -r b0de8551fadf -r c4e29a0bb8c1 src/Pure/Isar/constdefs.ML --- 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 => () diff -r b0de8551fadf -r c4e29a0bb8c1 src/Pure/Isar/element.ML --- 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 diff -r b0de8551fadf -r c4e29a0bb8c1 src/Pure/Isar/expression.ML --- 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 diff -r b0de8551fadf -r c4e29a0bb8c1 src/Pure/Isar/local_defs.ML --- 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 **) diff -r b0de8551fadf -r c4e29a0bb8c1 src/Pure/Isar/method.ML --- 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 *) diff -r b0de8551fadf -r c4e29a0bb8c1 src/Pure/Isar/proof.ML --- 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 diff -r b0de8551fadf -r c4e29a0bb8c1 src/Pure/Isar/specification.ML --- 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) diff -r b0de8551fadf -r c4e29a0bb8c1 src/Pure/Isar/theory_target.ML --- 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]; diff -r b0de8551fadf -r c4e29a0bb8c1 src/Tools/Code/code_preproc.ML --- 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) => diff -r b0de8551fadf -r c4e29a0bb8c1 src/Tools/induct.ML --- 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);