--- 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