--- a/src/HOL/Tools/datatype_realizer.ML Wed Mar 11 15:38:25 2009 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML Wed Mar 11 15:42:19 2009 +0100
@@ -128,8 +128,9 @@
val ind_name = Thm.get_name induction;
val vs = map (fn i => List.nth (pnames, i)) is;
val (thm', thy') = thy
- |> Sign.absolute_path
- |> PureThy.store_thm (Binding.name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm)
+ |> Sign.root_path
+ |> PureThy.store_thm
+ (Binding.qualified_name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm)
||> Sign.restore_naming thy;
val ivs = rev (Term.add_vars (Logic.varify (DatatypeProp.make_ind [descr] sorts)) []);
@@ -194,8 +195,8 @@
val exh_name = Thm.get_name exhaustion;
val (thm', thy') = thy
- |> Sign.absolute_path
- |> PureThy.store_thm (Binding.name (exh_name ^ "_P_correctness"), thm)
+ |> Sign.root_path
+ |> PureThy.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm)
||> Sign.restore_naming thy;
val P = Var (("P", 0), rT' --> HOLogic.boolT);