proper error generated for wrong mixfix
authorblanchet
Wed Apr 24 22:48:22 2013 +0200 (2013-04-24)
changeset 51768d2a236b10796
parent 51767 bbcdd8519253
child 51769 5c657ca97d99
proper error generated for wrong mixfix
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Apr 24 18:49:52 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Apr 24 22:48:22 2013 +0200
     1.3 @@ -183,9 +183,16 @@
     1.4      (* TODO: cleaner handling of fake contexts, without "background_theory" *)
     1.5      (*the "perhaps o try" below helps gracefully handles the case where the new type is defined in a
     1.6        locale and shadows an existing global type*)
     1.7 +
     1.8 +    fun add_fake_type spec mixfix =
     1.9 +      Sign.add_type no_defs_lthy (type_binding_of spec,
    1.10 +        length (type_args_named_constrained_of spec), mixfix);
    1.11 +
    1.12      val fake_thy =
    1.13 -      Theory.copy #> fold (fn spec => perhaps (try (Sign.add_type no_defs_lthy
    1.14 -          (type_binding_of spec, length (type_args_named_constrained_of spec), mixfix_of spec))))
    1.15 +      Theory.copy #> fold (fn spec => fn thy =>
    1.16 +          case try (add_fake_type spec (mixfix_of spec)) thy of
    1.17 +            SOME thy' => thy'
    1.18 +          | NONE => add_fake_type spec Mixfix.NoSyn thy)
    1.19          specs;
    1.20      val fake_lthy = Proof_Context.background_theory fake_thy no_defs_lthy;
    1.21