modernized structure Local_Defs;
authorwenzelm
Sun Mar 07 11:57:16 2010 +0100 (2010-03-07)
changeset 35624c4e29a0bb8c1
parent 35623 b0de8551fadf
child 35625 9c818cab0dd0
modernized structure Local_Defs;
src/HOL/Library/reflection.ML
src/HOL/NSA/transfer.ML
src/HOL/Tools/Function/mutual.ML
src/HOL/Tools/Function/scnp_reconstruct.ML
src/HOL/Tools/Groebner_Basis/normalizer_data.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
src/HOL/Tools/Quotient/quotient_def.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/res_axioms.ML
src/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOLCF/Tools/fixrec.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/code.ML
src/Pure/Isar/constdefs.ML
src/Pure/Isar/element.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/method.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/specification.ML
src/Pure/Isar/theory_target.ML
src/Tools/Code/code_preproc.ML
src/Tools/induct.ML
     1.1 --- a/src/HOL/Library/reflection.ML	Sat Mar 06 19:17:59 2010 +0000
     1.2 +++ b/src/HOL/Library/reflection.ML	Sun Mar 07 11:57:16 2010 +0100
     1.3 @@ -62,7 +62,7 @@
     1.4     fun tryext x = (x RS ext2 handle THM _ =>  x)
     1.5     val cong = (Goal.prove ctxt'' [] (map mk_def env)
     1.6                            (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
     1.7 -                          (fn x => LocalDefs.unfold_tac (#context x) (map tryext (#prems x))
     1.8 +                          (fn x => Local_Defs.unfold_tac (#context x) (map tryext (#prems x))
     1.9                                                          THEN rtac th' 1)) RS sym
    1.10  
    1.11     val (cong' :: vars') =
     2.1 --- a/src/HOL/NSA/transfer.ML	Sat Mar 06 19:17:59 2010 +0000
     2.2 +++ b/src/HOL/NSA/transfer.ML	Sun Mar 07 11:57:16 2010 +0100
     2.3 @@ -56,7 +56,7 @@
     2.4    let
     2.5      val thy = ProofContext.theory_of ctxt;
     2.6      val {intros,unfolds,refolds,consts} = TransferData.get (Context.Proof ctxt);
     2.7 -    val meta = LocalDefs.meta_rewrite_rule ctxt;
     2.8 +    val meta = Local_Defs.meta_rewrite_rule ctxt;
     2.9      val ths' = map meta ths;
    2.10      val unfolds' = map meta unfolds and refolds' = map meta refolds;
    2.11      val (_$_$t') = concl_of (MetaSimplifier.rewrite true unfolds' (cterm_of thy t))
     3.1 --- a/src/HOL/Tools/Function/mutual.ML	Sat Mar 06 19:17:59 2010 +0000
     3.2 +++ b/src/HOL/Tools/Function/mutual.ML	Sun Mar 07 11:57:16 2010 +0100
     3.3 @@ -190,7 +190,7 @@
     3.4    in
     3.5      Goal.prove ctxt [] []
     3.6        (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
     3.7 -      (fn _ => (LocalDefs.unfold_tac ctxt all_orig_fdefs)
     3.8 +      (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs)
     3.9           THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
    3.10           THEN (simp_tac (simpset_of ctxt addsimps SumTree.proj_in_rules)) 1)
    3.11      |> restore_cond
     4.1 --- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Sat Mar 06 19:17:59 2010 +0000
     4.2 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Sun Mar 07 11:57:16 2010 +0100
     4.3 @@ -123,7 +123,7 @@
     4.4  (* General reduction pair application *)
     4.5  fun rem_inv_img ctxt =
     4.6    let
     4.7 -    val unfold_tac = LocalDefs.unfold_tac ctxt
     4.8 +    val unfold_tac = Local_Defs.unfold_tac ctxt
     4.9    in
    4.10      rtac @{thm subsetI} 1
    4.11      THEN etac @{thm CollectE} 1
    4.12 @@ -259,7 +259,7 @@
    4.13              THEN mset_pwleq_tac 1
    4.14              THEN EVERY (map2 (less_proof false) qs ps)
    4.15              THEN (if strict orelse qs <> lq
    4.16 -                  then LocalDefs.unfold_tac ctxt set_of_simps
    4.17 +                  then Local_Defs.unfold_tac ctxt set_of_simps
    4.18                         THEN steps_tac MAX true
    4.19                         (subtract (op =) qs lq) (subtract (op =) ps lp)
    4.20                    else all_tac)
    4.21 @@ -290,7 +290,7 @@
    4.22           THEN (rtac (order_rpair ms_rp label) 1)
    4.23           THEN PRIMITIVE (instantiate' [] [SOME level_mapping])
    4.24           THEN unfold_tac @{thms rp_inv_image_def} (simpset_of ctxt)
    4.25 -         THEN LocalDefs.unfold_tac ctxt
    4.26 +         THEN Local_Defs.unfold_tac ctxt
    4.27             (@{thms split_conv} @ @{thms fst_conv} @ @{thms snd_conv})
    4.28           THEN REPEAT (SOMEGOAL (resolve_tac [@{thm Un_least}, @{thm empty_subsetI}]))
    4.29           THEN EVERY (map (prove_lev true) sl)
     5.1 --- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Sat Mar 06 19:17:59 2010 +0000
     5.2 +++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Sun Mar 07 11:57:16 2010 +0100
     5.3 @@ -127,7 +127,7 @@
     5.4          check_rules fieldN f_rules 2 andalso
     5.5          check_rules idomN idom 2;
     5.6  
     5.7 -      val mk_meta = LocalDefs.meta_rewrite_rule ctxt;
     5.8 +      val mk_meta = Local_Defs.meta_rewrite_rule ctxt;
     5.9        val sr_rules' = map mk_meta sr_rules;
    5.10        val r_rules' = map mk_meta r_rules;
    5.11        val f_rules' = map mk_meta f_rules;
     6.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Mar 06 19:17:59 2010 +0000
     6.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sun Mar 07 11:57:16 2010 +0100
     6.3 @@ -418,7 +418,7 @@
     6.4  *)
     6.5  fun prepare_split_thm ctxt split_thm =
     6.6      (split_thm RS @{thm iffD2})
     6.7 -    |> LocalDefs.unfold ctxt [@{thm atomize_conjL[symmetric]},
     6.8 +    |> Local_Defs.unfold ctxt [@{thm atomize_conjL[symmetric]},
     6.9        @{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}]
    6.10  
    6.11  fun find_split_thm thy (Const (name, typ)) =
     7.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Sat Mar 06 19:17:59 2010 +0000
     7.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Sun Mar 07 11:57:16 2010 +0100
     7.3 @@ -145,7 +145,7 @@
     7.4      val t' = Pattern.rewrite_term thy rewr [] t
     7.5      val tac = Skip_Proof.cheat_tac thy
     7.6      val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn _ => tac)
     7.7 -    val th''' = LocalDefs.unfold ctxt [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}] th''
     7.8 +    val th''' = Local_Defs.unfold ctxt [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}] th''
     7.9    in
    7.10      th'''
    7.11    end;
     8.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Sat Mar 06 19:17:59 2010 +0000
     8.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Sun Mar 07 11:57:16 2010 +0100
     8.3 @@ -63,7 +63,7 @@
     8.4    val qconst_bname = Binding.name lhs_str
     8.5    val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
     8.6    val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
     8.7 -  val (_, prop') = LocalDefs.cert_def lthy prop
     8.8 +  val (_, prop') = Local_Defs.cert_def lthy prop
     8.9    val (_, newrhs) = Primitive_Defs.abs_def prop'
    8.10  
    8.11    val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy
     9.1 --- a/src/HOL/Tools/inductive.ML	Sat Mar 06 19:17:59 2010 +0000
     9.2 +++ b/src/HOL/Tools/inductive.ML	Sun Mar 07 11:57:16 2010 +0100
     9.3 @@ -832,7 +832,7 @@
     9.4          let
     9.5            val _ = Binding.is_empty name andalso null atts orelse
     9.6              error "Abbreviations may not have names or attributes";
     9.7 -          val ((x, T), rhs) = LocalDefs.abs_def (snd (LocalDefs.cert_def ctxt1 t));
     9.8 +          val ((x, T), rhs) = Local_Defs.abs_def (snd (Local_Defs.cert_def ctxt1 t));
     9.9            val var =
    9.10              (case find_first (fn ((c, _), _) => Binding.name_of c = x) cnames_syn of
    9.11                NONE => error ("Undeclared head of abbreviation " ^ quote x)
    9.12 @@ -854,8 +854,8 @@
    9.13      val ps = map Free pnames;
    9.14  
    9.15      val (_, ctxt2) = lthy |> Variable.add_fixes (map (Binding.name_of o fst o fst) cnames_syn');
    9.16 -    val _ = map (fn abbr => LocalDefs.fixed_abbrev abbr ctxt2) abbrevs;
    9.17 -    val ctxt3 = ctxt2 |> fold (snd oo LocalDefs.fixed_abbrev) abbrevs;
    9.18 +    val _ = map (fn abbr => Local_Defs.fixed_abbrev abbr ctxt2) abbrevs;
    9.19 +    val ctxt3 = ctxt2 |> fold (snd oo Local_Defs.fixed_abbrev) abbrevs;
    9.20      val expand = Assumption.export_term ctxt3 lthy #> ProofContext.cert_term lthy;
    9.21  
    9.22      fun close_rule r = list_all_free (rev (fold_aterms
    10.1 --- a/src/HOL/Tools/res_axioms.ML	Sat Mar 06 19:17:59 2010 +0000
    10.2 +++ b/src/HOL/Tools/res_axioms.ML	Sun Mar 07 11:57:16 2010 +0100
    10.3 @@ -475,7 +475,7 @@
    10.4                                        (map Thm.term_of hyps)
    10.5        val fixed = OldTerm.term_frees (concl_of st) @
    10.6                    fold (union (op aconv)) (map OldTerm.term_frees remaining_hyps) []
    10.7 -  in Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
    10.8 +  in Seq.of_list [Local_Defs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
    10.9  
   10.10  
   10.11  fun meson_general_tac ctxt ths i st0 =
    11.1 --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Sat Mar 06 19:17:59 2010 +0000
    11.2 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Mar 07 11:57:16 2010 +0100
    11.3 @@ -174,7 +174,7 @@
    11.4          (K (beta_tac 1));
    11.5      val tuple_unfold_thm =
    11.6        (@{thm def_cont_fix_eq} OF [tuple_fixdef_thm, cont_thm])
    11.7 -      |> LocalDefs.unfold (ProofContext.init thy) @{thms split_conv};
    11.8 +      |> Local_Defs.unfold (ProofContext.init thy) @{thms split_conv};
    11.9  
   11.10      fun mk_unfold_thms [] thm = []
   11.11        | mk_unfold_thms (n::[]) thm = [(n, thm)]
    12.1 --- a/src/HOLCF/Tools/fixrec.ML	Sat Mar 06 19:17:59 2010 +0000
    12.2 +++ b/src/HOLCF/Tools/fixrec.ML	Sun Mar 07 11:57:16 2010 +0100
    12.3 @@ -146,9 +146,9 @@
    12.4      val predicate = lambda_tuple lhss (list_comb (P, lhss));
    12.5      val tuple_induct_thm = (def_cont_fix_ind OF [tuple_fixdef_thm, cont_thm])
    12.6        |> Drule.instantiate' [] [SOME (Thm.cterm_of thy predicate)]
    12.7 -      |> LocalDefs.unfold lthy @{thms split_paired_all split_conv split_strict};
    12.8 +      |> Local_Defs.unfold lthy @{thms split_paired_all split_conv split_strict};
    12.9      val tuple_unfold_thm = (def_cont_fix_eq OF [tuple_fixdef_thm, cont_thm])
   12.10 -      |> LocalDefs.unfold lthy' @{thms split_conv};
   12.11 +      |> Local_Defs.unfold lthy' @{thms split_conv};
   12.12      fun unfolds [] thm = []
   12.13        | unfolds (n::[]) thm = [(n, thm)]
   12.14        | unfolds (n::ns) thm = let
    13.1 --- a/src/Pure/Isar/attrib.ML	Sat Mar 06 19:17:59 2010 +0000
    13.2 +++ b/src/Pure/Isar/attrib.ML	Sun Mar 07 11:57:16 2010 +0100
    13.3 @@ -245,8 +245,8 @@
    13.4  fun unfolded_syntax rule =
    13.5    thms >> (fn ths => Thm.rule_attribute (fn context => rule (Context.proof_of context) ths));
    13.6  
    13.7 -val unfolded = unfolded_syntax LocalDefs.unfold;
    13.8 -val folded = unfolded_syntax LocalDefs.fold;
    13.9 +val unfolded = unfolded_syntax Local_Defs.unfold;
   13.10 +val folded = unfolded_syntax Local_Defs.fold;
   13.11  
   13.12  
   13.13  (* rule format *)
   13.14 @@ -311,7 +311,7 @@
   13.15    setup (Binding.name "rulify") (Scan.succeed ObjectLogic.declare_rulify)
   13.16      "declaration of rulify rule" #>
   13.17    setup (Binding.name "rotated") (Scan.lift rotated) "rotated theorem premises" #>
   13.18 -  setup (Binding.name "defn") (add_del LocalDefs.defn_add LocalDefs.defn_del)
   13.19 +  setup (Binding.name "defn") (add_del Local_Defs.defn_add Local_Defs.defn_del)
   13.20      "declaration of definitional transformations" #>
   13.21    setup (Binding.name "abs_def") (Scan.succeed (Thm.rule_attribute (K Drule.abs_def)))
   13.22      "abstract over free variables of a definition"));
    14.1 --- a/src/Pure/Isar/code.ML	Sat Mar 06 19:17:59 2010 +0000
    14.2 +++ b/src/Pure/Isar/code.ML	Sun Mar 07 11:57:16 2010 +0100
    14.3 @@ -566,7 +566,7 @@
    14.4  
    14.5  fun assert_eqn thy = error_thm (gen_assert_eqn thy true);
    14.6  
    14.7 -fun meta_rewrite thy = LocalDefs.meta_rewrite_rule (ProofContext.init thy);
    14.8 +fun meta_rewrite thy = Local_Defs.meta_rewrite_rule (ProofContext.init thy);
    14.9  
   14.10  fun mk_eqn thy = error_thm (gen_assert_eqn thy false) o
   14.11    apfst (meta_rewrite thy);
   14.12 @@ -810,7 +810,7 @@
   14.13          val tyscm = typscheme_of_cert thy cert;
   14.14          val thms = if null propers then [] else
   14.15            cert_thm
   14.16 -          |> LocalDefs.expand [snd (get_head thy cert_thm)]
   14.17 +          |> Local_Defs.expand [snd (get_head thy cert_thm)]
   14.18            |> Thm.varifyT
   14.19            |> Conjunction.elim_balanced (length propers);
   14.20        in (tyscm, map (pair NONE o dest_eqn thy o Thm.prop_of) thms ~~ (map SOME thms ~~ propers)) end
    15.1 --- a/src/Pure/Isar/constdefs.ML	Sat Mar 06 19:17:59 2010 +0000
    15.2 +++ b/src/Pure/Isar/constdefs.ML	Sun Mar 07 11:57:16 2010 +0100
    15.3 @@ -34,7 +34,7 @@
    15.4              ProofContext.add_fixes [(x, T, mx)] #> snd #> pair (SOME x, mx)));
    15.5  
    15.6      val prop = prep_prop var_ctxt raw_prop;
    15.7 -    val (c, T) = #1 (LocalDefs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
    15.8 +    val (c, T) = #1 (Local_Defs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
    15.9      val _ =
   15.10        (case Option.map Name.of_binding d of
   15.11          NONE => ()
    16.1 --- a/src/Pure/Isar/element.ML	Sat Mar 06 19:17:59 2010 +0000
    16.2 +++ b/src/Pure/Isar/element.ML	Sun Mar 07 11:57:16 2010 +0100
    16.3 @@ -499,11 +499,11 @@
    16.4        let
    16.5          val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
    16.6          val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
    16.7 -            let val ((c, _), t') = LocalDefs.cert_def ctxt t  (* FIXME adapt ps? *)
    16.8 +            let val ((c, _), t') = Local_Defs.cert_def ctxt t  (* FIXME adapt ps? *)
    16.9              in (t', ((Thm.def_binding_optional (Binding.name c) name, atts), [(t', ps)])) end);
   16.10          val (_, ctxt') = ctxt
   16.11            |> fold Variable.auto_fixes (map #1 asms)
   16.12 -          |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
   16.13 +          |> ProofContext.add_assms_i Local_Defs.def_export (map #2 asms);
   16.14        in ctxt' end)
   16.15    | init (Notes (kind, facts)) = (fn context =>
   16.16        let
    17.1 --- a/src/Pure/Isar/expression.ML	Sat Mar 06 19:17:59 2010 +0000
    17.2 +++ b/src/Pure/Isar/expression.ML	Sun Mar 07 11:57:16 2010 +0100
    17.3 @@ -298,7 +298,7 @@
    17.4            Assumes asms => Assumes (asms |> map (fn (a, propps) =>
    17.5              (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
    17.6          | Defines defs => Defines (defs |> map (fn ((name, atts), (t, ps)) =>
    17.7 -            let val ((c, _), t') = LocalDefs.cert_def ctxt (close_frees t)
    17.8 +            let val ((c, _), t') = Local_Defs.cert_def ctxt (close_frees t)
    17.9              in ((Thm.def_binding_optional (Binding.name c) name, atts), (t', no_binds ps)) end))
   17.10          | e => e)
   17.11        end;
   17.12 @@ -513,8 +513,8 @@
   17.13  
   17.14  fun bind_def ctxt eq (xs, env, eqs) =
   17.15    let
   17.16 -    val _ = LocalDefs.cert_def ctxt eq;
   17.17 -    val ((y, T), b) = LocalDefs.abs_def eq;
   17.18 +    val _ = Local_Defs.cert_def ctxt eq;
   17.19 +    val ((y, T), b) = Local_Defs.abs_def eq;
   17.20      val b' = norm_term env b;
   17.21      fun err msg = error (msg ^ ": " ^ quote y);
   17.22    in
   17.23 @@ -808,8 +808,8 @@
   17.24          val eqns = map (Morphism.thm (export' $> export)) raw_eqns;
   17.25          val eqn_attrss = map2 (fn attrs => fn eqn =>
   17.26            ((apsnd o map) (Attrib.attribute_i thy) attrs, [([eqn], [])])) attrss eqns;
   17.27 -        fun meta_rewrite thy = map (LocalDefs.meta_rewrite_rule (ProofContext.init thy) #>
   17.28 -          Drule.abs_def) o maps snd;
   17.29 +        fun meta_rewrite thy =
   17.30 +          map (Local_Defs.meta_rewrite_rule (ProofContext.init thy) #> Drule.abs_def) o maps snd;
   17.31        in
   17.32          thy
   17.33          |> PureThy.note_thmss Thm.lemmaK eqn_attrss
    18.1 --- a/src/Pure/Isar/local_defs.ML	Sat Mar 06 19:17:59 2010 +0000
    18.2 +++ b/src/Pure/Isar/local_defs.ML	Sun Mar 07 11:57:16 2010 +0100
    18.3 @@ -34,7 +34,7 @@
    18.4      ((string * typ) * term) * (Proof.context -> thm -> thm)
    18.5  end;
    18.6  
    18.7 -structure LocalDefs: LOCAL_DEFS =
    18.8 +structure Local_Defs: LOCAL_DEFS =
    18.9  struct
   18.10  
   18.11  (** primitive definitions **)
    19.1 --- a/src/Pure/Isar/method.ML	Sat Mar 06 19:17:59 2010 +0000
    19.2 +++ b/src/Pure/Isar/method.ML	Sun Mar 07 11:57:16 2010 +0100
    19.3 @@ -165,8 +165,8 @@
    19.4  
    19.5  (* unfold/fold definitions *)
    19.6  
    19.7 -fun unfold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (LocalDefs.unfold_tac ctxt ths));
    19.8 -fun fold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (LocalDefs.fold_tac ctxt ths));
    19.9 +fun unfold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (Local_Defs.unfold_tac ctxt ths));
   19.10 +fun fold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (Local_Defs.fold_tac ctxt ths));
   19.11  
   19.12  
   19.13  (* atomize rule statements *)
    20.1 --- a/src/Pure/Isar/proof.ML	Sat Mar 06 19:17:59 2010 +0000
    20.2 +++ b/src/Pure/Isar/proof.ML	Sun Mar 07 11:57:16 2010 +0100
    20.3 @@ -599,7 +599,7 @@
    20.4      |>> map (fn (x, _, mx) => (x, mx))
    20.5      |-> (fn vars =>
    20.6        map_context_result (prep_binds false (map swap raw_rhss))
    20.7 -      #-> (fn rhss => map_context_result (LocalDefs.add_defs (vars ~~ (name_atts ~~ rhss)))))
    20.8 +      #-> (fn rhss => map_context_result (Local_Defs.add_defs (vars ~~ (name_atts ~~ rhss)))))
    20.9      |-> (put_facts o SOME o map (#2 o #2))
   20.10    end;
   20.11  
   20.12 @@ -681,8 +681,8 @@
   20.13        in (statement, [], f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end));
   20.14  
   20.15  fun append_using _ ths using = using @ filter_out Thm.is_dummy ths;
   20.16 -fun unfold_using ctxt ths = map (LocalDefs.unfold ctxt ths);
   20.17 -val unfold_goals = LocalDefs.unfold_goals;
   20.18 +fun unfold_using ctxt ths = map (Local_Defs.unfold ctxt ths);
   20.19 +val unfold_goals = Local_Defs.unfold_goals;
   20.20  
   20.21  in
   20.22  
    21.1 --- a/src/Pure/Isar/specification.ML	Sat Mar 06 19:17:59 2010 +0000
    21.2 +++ b/src/Pure/Isar/specification.ML	Sun Mar 07 11:57:16 2010 +0100
    21.3 @@ -193,7 +193,7 @@
    21.4  fun gen_def do_print prep (raw_var, raw_spec) lthy =
    21.5    let
    21.6      val (vars, [((raw_name, atts), prop)]) = fst (prep (the_list raw_var) [raw_spec] lthy);
    21.7 -    val (((x, T), rhs), prove) = LocalDefs.derived_def lthy true prop;
    21.8 +    val (((x, T), rhs), prove) = Local_Defs.derived_def lthy true prop;
    21.9      val var as (b, _) =
   21.10        (case vars of
   21.11          [] => (Binding.name x, NoSyn)
   21.12 @@ -232,7 +232,7 @@
   21.13      val ((vars, [(_, prop)]), _) =
   21.14        prep (the_list raw_var) [(Attrib.empty_binding, raw_prop)]
   21.15          (lthy |> ProofContext.set_mode ProofContext.mode_abbrev);
   21.16 -    val ((x, T), rhs) = LocalDefs.abs_def (#2 (LocalDefs.cert_def lthy prop));
   21.17 +    val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy prop));
   21.18      val var =
   21.19        (case vars of
   21.20          [] => (Binding.name x, NoSyn)
    22.1 --- a/src/Pure/Isar/theory_target.ML	Sat Mar 06 19:17:59 2010 +0000
    22.2 +++ b/src/Pure/Isar/theory_target.ML	Sun Mar 07 11:57:16 2010 +0100
    22.3 @@ -121,7 +121,7 @@
    22.4  
    22.5      (*export assumes/defines*)
    22.6      val th = Goal.norm_result raw_th;
    22.7 -    val (defs, th') = LocalDefs.export ctxt thy_ctxt th;
    22.8 +    val (defs, th') = Local_Defs.export ctxt thy_ctxt th;
    22.9      val concl_conv = MetaSimplifier.rewrite true defs (Thm.cprop_of th);
   22.10      val assms = map (MetaSimplifier.rewrite_rule defs o Thm.assume) (Assumption.all_assms_of ctxt);
   22.11      val nprems = Thm.nprems_of th' - Thm.nprems_of th;
   22.12 @@ -152,7 +152,7 @@
   22.13      val result'' =
   22.14        (case SINGLE (Seq.INTERVAL assm_tac 1 nprems) result' of
   22.15          NONE => raise THM ("Failed to re-import result", 0, [result'])
   22.16 -      | SOME res => LocalDefs.trans_props ctxt [res, Thm.symmetric concl_conv])
   22.17 +      | SOME res => Local_Defs.trans_props ctxt [res, Thm.symmetric concl_conv])
   22.18        |> Goal.norm_result
   22.19        |> PureThy.name_thm false false name;
   22.20  
   22.21 @@ -235,7 +235,7 @@
   22.22      lthy'
   22.23      |> is_locale ? term_syntax ta false (locale_const ta Syntax.mode_default ((b, mx2), t))
   22.24      |> is_class ? class_target ta (Class_Target.declare target ((b, mx1), t))
   22.25 -    |> LocalDefs.add_def ((b, NoSyn), t)
   22.26 +    |> Local_Defs.add_def ((b, NoSyn), t)
   22.27    end;
   22.28  
   22.29  
   22.30 @@ -266,7 +266,7 @@
   22.31            (Sign.add_abbrev (#1 prmode) (b, global_rhs) #-> (fn (lhs, _) =>
   22.32             Sign.notation true prmode [(lhs, mx3)])))
   22.33      |> ProofContext.add_abbrev PrintMode.internal (b, t) |> snd
   22.34 -    |> LocalDefs.fixed_abbrev ((b, NoSyn), t)
   22.35 +    |> Local_Defs.fixed_abbrev ((b, NoSyn), t)
   22.36    end;
   22.37  
   22.38  
   22.39 @@ -279,7 +279,7 @@
   22.40  
   22.41      val name' = Thm.def_binding_optional b name;
   22.42      val (rhs', rhs_conv) =
   22.43 -      LocalDefs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
   22.44 +      Local_Defs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
   22.45      val xs = Variable.add_fixed (Local_Theory.target_of lthy) rhs' [];
   22.46      val T = Term.fastype_of rhs;
   22.47  
   22.48 @@ -296,7 +296,7 @@
   22.49              if is_none (Class_Target.instantiation_param lthy b)
   22.50              then Thm.add_def false false (name', Logic.mk_equals (lhs', rhs'))
   22.51              else AxClass.define_overloaded name' (fst (dest_Const lhs'), rhs'));
   22.52 -    val def = LocalDefs.trans_terms lthy3
   22.53 +    val def = Local_Defs.trans_terms lthy3
   22.54        [(*c == global.c xs*)     local_def,
   22.55         (*global.c xs == rhs'*)  global_def,
   22.56         (*rhs' == rhs*)          Thm.symmetric rhs_conv];
    23.1 --- a/src/Tools/Code/code_preproc.ML	Sat Mar 06 19:17:59 2010 +0000
    23.2 +++ b/src/Tools/Code/code_preproc.ML	Sun Mar 07 11:57:16 2010 +0100
    23.3 @@ -87,7 +87,7 @@
    23.4  
    23.5  fun add_unfold_post raw_thm thy =
    23.6    let
    23.7 -    val thm = LocalDefs.meta_rewrite_rule (ProofContext.init thy) raw_thm;
    23.8 +    val thm = Local_Defs.meta_rewrite_rule (ProofContext.init thy) raw_thm;
    23.9      val thm_sym = Thm.symmetric thm;
   23.10    in
   23.11      thy |> map_pre_post (fn (pre, post) =>
    24.1 --- a/src/Tools/induct.ML	Sat Mar 06 19:17:59 2010 +0000
    24.2 +++ b/src/Tools/induct.ML	Sun Mar 07 11:57:16 2010 +0100
    24.3 @@ -683,14 +683,14 @@
    24.4      fun add (SOME (_, (t, true))) ctxt = ((SOME t, []), ctxt)
    24.5        | add (SOME (SOME x, (t, _))) ctxt =
    24.6            let val ([(lhs, (_, th))], ctxt') =
    24.7 -            LocalDefs.add_defs [((x, NoSyn), (Thm.empty_binding, t))] ctxt
    24.8 +            Local_Defs.add_defs [((x, NoSyn), (Thm.empty_binding, t))] ctxt
    24.9            in ((SOME lhs, [th]), ctxt') end
   24.10        | add (SOME (NONE, (t as Free _, _))) ctxt = ((SOME t, []), ctxt)
   24.11        | add (SOME (NONE, (t, _))) ctxt =
   24.12            let
   24.13              val ([s], _) = Name.variants ["x"] (Variable.names_of ctxt);
   24.14              val ([(lhs, (_, th))], ctxt') =
   24.15 -              LocalDefs.add_defs [((Binding.name s, NoSyn),
   24.16 +              Local_Defs.add_defs [((Binding.name s, NoSyn),
   24.17                  (Thm.empty_binding, t))] ctxt
   24.18            in ((SOME lhs, [th]), ctxt') end
   24.19        | add NONE ctxt = ((NONE, []), ctxt);