src/HOLCF/Tools/pcpodef.ML
changeset 33671 4b0f2599ed48
parent 33646 d2f3104ca3d2
child 33680 a47277e09012
     1.1 --- a/src/HOLCF/Tools/pcpodef.ML	Fri Nov 13 20:41:29 2009 +0100
     1.2 +++ b/src/HOLCF/Tools/pcpodef.ML	Fri Nov 13 21:11:15 2009 +0100
     1.3 @@ -201,7 +201,7 @@
     1.4      val thy5 = lthy4
     1.5        |> Class.prove_instantiation_instance
     1.6            (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_definition]) 1))
     1.7 -      |> LocalTheory.exit_global;
     1.8 +      |> Local_Theory.exit_global;
     1.9    in ((info, below_definition), thy5) end;
    1.10  
    1.11  fun prepare_cpodef