--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Sep 23 09:36:18 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Sep 23 09:50:38 2015 +0200
@@ -198,9 +198,8 @@
val final_fqn = Sign.full_name thy binding
val tyargs =
List.tabulate (arity, rpair @{sort type} o prefix "'" o string_of_int)
- val thy' =
- Typedecl.typedecl_global true (mk_binding config type_name, tyargs, NoSyn) thy
- |> snd
+ val (_, thy') =
+ Typedecl.typedecl_global {final = true} (mk_binding config type_name, tyargs, NoSyn) thy
val typ_map_entry = (thf_type, (final_fqn, arity))
val ty_map' = typ_map_entry :: ty_map
in (ty_map', thy') end