--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed Apr 24 18:49:52 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed Apr 24 22:48:22 2013 +0200
@@ -183,9 +183,16 @@
(* TODO: cleaner handling of fake contexts, without "background_theory" *)
(*the "perhaps o try" below helps gracefully handles the case where the new type is defined in a
locale and shadows an existing global type*)
+
+ fun add_fake_type spec mixfix =
+ Sign.add_type no_defs_lthy (type_binding_of spec,
+ length (type_args_named_constrained_of spec), mixfix);
+
val fake_thy =
- Theory.copy #> fold (fn spec => perhaps (try (Sign.add_type no_defs_lthy
- (type_binding_of spec, length (type_args_named_constrained_of spec), mixfix_of spec))))
+ Theory.copy #> fold (fn spec => fn thy =>
+ case try (add_fake_type spec (mixfix_of spec)) thy of
+ SOME thy' => thy'
+ | NONE => add_fake_type spec Mixfix.NoSyn thy)
specs;
val fake_lthy = Proof_Context.background_theory fake_thy no_defs_lthy;