# HG changeset patch
# User huffman
# Date 1258157404 28800
# Node ID cddea85bc87b8829ad32b2cff9c7fd9df2080779
# Parent  a47277e0901288fb40c0c2b813932a7a5d1e1ad7
LocalTheory -> Local_Theory

diff -r a47277e09012 -r cddea85bc87b src/HOLCF/Tools/repdef.ML
--- a/src/HOLCF/Tools/repdef.ML	Fri Nov 13 15:40:06 2009 -0800
+++ b/src/HOLCF/Tools/repdef.ML	Fri Nov 13 16:10:04 2009 -0800
@@ -126,7 +126,7 @@
     val thy4 = lthy3
       |> Class.prove_instantiation_instance
           (K (Tactic.rtac (@{thm typedef_rep_class} OF typedef_thms) 1))
-      |> LocalTheory.exit_global;
+      |> Local_Theory.exit_global;
 
     (*other theorems*)
     val typedef_thms' = map (Thm.transfer thy4)