# HG changeset patch
# User wenzelm
# Date 948828177 -3600
# Node ID d6d896e81cd74438a3bc49bc56eee496eb2f0a1f
# Parent  80a24574dced105ba4cc8fd737d8d97671f19530
fallback on PureThy version;

diff -r 80a24574dced -r d6d896e81cd7 src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Tue Jan 25 09:25:43 2000 +0100
+++ b/src/HOL/Tools/typedef_package.ML	Tue Jan 25 20:22:57 2000 +0100
@@ -34,9 +34,11 @@
     fun arity_of (raw_name, args, mx) =
       (full (Syntax.type_name raw_name mx), replicate (length args) HOLogic.termS, HOLogic.termS);
   in
-    thy
-    |> PureThy.add_typedecls decls
-    |> Theory.add_arities_i (map arity_of decls)
+    if can (Theory.assert_super HOL.thy) thy then
+      thy
+      |> PureThy.add_typedecls decls
+      |> Theory.add_arities_i (map arity_of decls)
+    else thy |> PureThy.add_typedecls decls
   end;