src/HOL/Statespace/state_space.ML
changeset 36610 bafd82950e24
parent 36506 6b56e679d9ff
child 36692 54b64d4ad524
     1.1 --- a/src/HOL/Statespace/state_space.ML	Mon May 03 07:59:51 2010 +0200
     1.2 +++ b/src/HOL/Statespace/state_space.ML	Mon May 03 14:25:56 2010 +0200
     1.3 @@ -440,7 +440,7 @@
     1.4  
     1.5     fun string_of_typ T =
     1.6        setmp_CRITICAL show_sorts true
     1.7 -       (PrintMode.setmp [] (Syntax.string_of_typ (ProofContext.init thy))) T;
     1.8 +       (PrintMode.setmp [] (Syntax.string_of_typ (ProofContext.init_global thy))) T;
     1.9     val fixestate = (case state_type of
    1.10           NONE => []
    1.11         | SOME s =>
    1.12 @@ -502,7 +502,7 @@
    1.13        *)
    1.14      val _ = writeln ("Defining statespace " ^ quote name ^ " ...");
    1.15  
    1.16 -    val ctxt = ProofContext.init thy;
    1.17 +    val ctxt = ProofContext.init_global thy;
    1.18  
    1.19      fun add_parent (Ts,pname,rs) env =
    1.20        let