src/HOL/Tools/typedef_package.ML

--- a/src/HOL/Tools/typedef_package.ML	Mon Nov 27 23:48:10 2006 +0100
+++ b/src/HOL/Tools/typedef_package.ML	Tue Nov 28 00:35:18 2006 +0100
@@ -54,9 +54,9 @@
       replicate (length args) HOLogic.typeS, HOLogic.typeS);
 
 fun add_typedecls decls thy =
-  thy
-  |> Theory.add_typedecls decls
-  |> can (Theory.assert_super HOL.thy) ? fold HOL_arity decls;
+  if can (Theory.assert_super HOL.thy) thy then
+    thy |> Theory.add_typedecls decls |> fold HOL_arity decls
+  else thy |> Theory.add_typedecls decls;