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