Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Datatype/datatype.ML
changeset 40929 7ff03a5e044f
parent 40719 acb830207103
child 41423 25df154b8ffc 
--- a/src/HOL/Tools/Datatype/datatype.ML	Fri Dec 03 10:03:10 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Dec 03 10:03:13 2010 +0100
@@ -628,9 +628,9 @@
 
     val ([dt_induct'], thy7) =
       thy6
-      |> Sign.add_path big_name
-      |> Global_Theory.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])]
-      ||> Sign.parent_path
+      |> Global_Theory.add_thms
+        [((Binding.qualify true big_name (Binding.name "induct"), dt_induct),
+          [case_names_induct])]
       ||> Theory.checkpoint;
 
   in
isabelle