src/HOL/Tools/old_primrec_package.ML
changeset 29579 cb520b766e00
parent 29290 8fb767245822
child 29870 2dea33c62da7
--- a/src/HOL/Tools/old_primrec_package.ML	Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/Tools/old_primrec_package.ML	Wed Jan 21 16:47:04 2009 +0100
@@ -305,11 +305,11 @@
   end;
 
 fun thy_note ((name, atts), thms) =
-  PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
+  PureThy.add_thmss [((Binding.name name, thms), atts)] #-> (fn [thms] => pair (name, thms));
 fun thy_def false ((name, atts), t) =
-      PureThy.add_defs false [((name, t), atts)] #-> (fn [thm] => pair (name, thm))
+      PureThy.add_defs false [((Binding.name name, t), atts)] #-> (fn [thm] => pair (name, thm))
   | thy_def true ((name, atts), t) =
-      PureThy.add_defs_unchecked false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
+      PureThy.add_defs_unchecked false [((Binding.name name, t), atts)] #-> (fn [thm] => pair (name, thm));
 
 in