1.1 --- a/src/HOL/Tools/typedef_package.ML	Tue Jan 25 09:25:43 2000 +0100
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Tue Jan 25 20:22:57 2000 +0100
     1.3 @@ -34,9 +34,11 @@
     1.4      fun arity_of (raw_name, args, mx) =
     1.5        (full (Syntax.type_name raw_name mx), replicate (length args) HOLogic.termS, HOLogic.termS);
     1.6    in
     1.7 -    thy
     1.8 -    |> PureThy.add_typedecls decls
     1.9 -    |> Theory.add_arities_i (map arity_of decls)
    1.10 +    if can (Theory.assert_super HOL.thy) thy then
    1.11 +      thy
    1.12 +      |> PureThy.add_typedecls decls
    1.13 +      |> Theory.add_arities_i (map arity_of decls)
    1.14 +    else thy |> PureThy.add_typedecls decls
    1.15    end;
    1.16  
    1.17