--- a/src/HOL/Tools/Function/size.ML Sat Apr 16 15:47:52 2011 +0200
+++ b/src/HOL/Tools/Function/size.ML Sat Apr 16 16:15:37 2011 +0200
@@ -133,8 +133,8 @@
val (thm, lthy') = lthy
|> Local_Theory.define ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs))
|-> (fn (t, (_, thm)) => Spec_Rules.add Spec_Rules.Equational ([t], [thm]) #> pair thm);
- val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy');
- val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
+ val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy');
+ val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm;
in (thm', lthy') end;
val ((size_def_thms, size_def_thms'), thy') =
@@ -152,7 +152,7 @@
||> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
||> Local_Theory.exit_global;
- val ctxt = ProofContext.init_global thy';
+ val ctxt = Proof_Context.init_global thy';
val simpset1 = HOL_basic_ss addsimps @{thm Nat.add_0} :: @{thm Nat.add_0_right} ::
size_def_thms @ size_def_thms' @ rec_rewrites @ extra_rewrites;