src/HOLCF/Tools/repdef.ML

--- a/src/HOLCF/Tools/repdef.ML	Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOLCF/Tools/repdef.ML	Mon Sep 20 16:05:25 2010 +0200
@@ -139,7 +139,7 @@
       [type_definition_thm, #below_def cpo_info, emb_def, prj_def];
     val (REP_thm, thy) = thy
       |> Sign.add_path (Binding.name_of name)
-      |> PureThy.add_thm
+      |> Global_Theory.add_thm
          ((Binding.prefix_name "REP_" name,
           Drule.zero_var_indexes (@{thm typedef_REP} OF typedef_thms')), [])
       ||> Sign.restore_naming thy;