src/HOLCF/Tools/repdef.ML

--- a/src/HOLCF/Tools/repdef.ML	Tue Apr 20 22:34:17 2010 +0200
+++ b/src/HOLCF/Tools/repdef.ML	Tue Apr 20 13:44:28 2010 -0700
@@ -141,7 +141,7 @@
       |> Sign.add_path (Binding.name_of name)
       |> PureThy.add_thm
          ((Binding.prefix_name "REP_" name,
-          Drule.export_without_context (@{thm typedef_REP} OF typedef_thms')), [])
+          Drule.zero_var_indexes (@{thm typedef_REP} OF typedef_thms')), [])
       ||> Sign.restore_naming thy;
 
     val rep_info =