src/Pure/Isar/expression.ML
changeset 35624 c4e29a0bb8c1
parent 35262 9ea4445d2ccf
child 35625 9c818cab0dd0
     1.1 --- a/src/Pure/Isar/expression.ML	Sat Mar 06 19:17:59 2010 +0000
     1.2 +++ b/src/Pure/Isar/expression.ML	Sun Mar 07 11:57:16 2010 +0100
     1.3 @@ -298,7 +298,7 @@
     1.4            Assumes asms => Assumes (asms |> map (fn (a, propps) =>
     1.5              (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
     1.6          | Defines defs => Defines (defs |> map (fn ((name, atts), (t, ps)) =>
     1.7 -            let val ((c, _), t') = LocalDefs.cert_def ctxt (close_frees t)
     1.8 +            let val ((c, _), t') = Local_Defs.cert_def ctxt (close_frees t)
     1.9              in ((Thm.def_binding_optional (Binding.name c) name, atts), (t', no_binds ps)) end))
    1.10          | e => e)
    1.11        end;
    1.12 @@ -513,8 +513,8 @@
    1.13  
    1.14  fun bind_def ctxt eq (xs, env, eqs) =
    1.15    let
    1.16 -    val _ = LocalDefs.cert_def ctxt eq;
    1.17 -    val ((y, T), b) = LocalDefs.abs_def eq;
    1.18 +    val _ = Local_Defs.cert_def ctxt eq;
    1.19 +    val ((y, T), b) = Local_Defs.abs_def eq;
    1.20      val b' = norm_term env b;
    1.21      fun err msg = error (msg ^ ": " ^ quote y);
    1.22    in
    1.23 @@ -808,8 +808,8 @@
    1.24          val eqns = map (Morphism.thm (export' $> export)) raw_eqns;
    1.25          val eqn_attrss = map2 (fn attrs => fn eqn =>
    1.26            ((apsnd o map) (Attrib.attribute_i thy) attrs, [([eqn], [])])) attrss eqns;
    1.27 -        fun meta_rewrite thy = map (LocalDefs.meta_rewrite_rule (ProofContext.init thy) #>
    1.28 -          Drule.abs_def) o maps snd;
    1.29 +        fun meta_rewrite thy =
    1.30 +          map (Local_Defs.meta_rewrite_rule (ProofContext.init thy) #> Drule.abs_def) o maps snd;
    1.31        in
    1.32          thy
    1.33          |> PureThy.note_thmss Thm.lemmaK eqn_attrss