--- a/src/HOL/Statespace/state_space.ML Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML Mon May 03 14:25:56 2010 +0200
@@ -440,7 +440,7 @@
fun string_of_typ T =
setmp_CRITICAL show_sorts true
- (PrintMode.setmp [] (Syntax.string_of_typ (ProofContext.init thy))) T;
+ (PrintMode.setmp [] (Syntax.string_of_typ (ProofContext.init_global thy))) T;
val fixestate = (case state_type of
NONE => []
| SOME s =>
@@ -502,7 +502,7 @@
*)
val _ = writeln ("Defining statespace " ^ quote name ^ " ...");
- val ctxt = ProofContext.init thy;
+ val ctxt = ProofContext.init_global thy;
fun add_parent (Ts,pname,rs) env =
let