simplified code -- no need for two attempts, the error we get from mixfix the first time is good (and better to get than a parse error in the specification because the user tries to use a mixfix that silently failed)
authorblanchet
Thu Apr 25 08:56:10 2013 +0200 (2013-04-25)
changeset 517695c657ca97d99
parent 51768 d2a236b10796
child 51770 78162d9e977d
simplified code -- no need for two attempts, the error we get from mixfix the first time is good (and better to get than a parse error in the specification because the user tries to use a mixfix that silently failed)
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Apr 24 22:48:22 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Apr 25 08:56:10 2013 +0200
     1.3 @@ -184,16 +184,11 @@
     1.4      (*the "perhaps o try" below helps gracefully handles the case where the new type is defined in a
     1.5        locale and shadows an existing global type*)
     1.6  
     1.7 -    fun add_fake_type spec mixfix =
     1.8 +    fun add_fake_type spec =
     1.9        Sign.add_type no_defs_lthy (type_binding_of spec,
    1.10 -        length (type_args_named_constrained_of spec), mixfix);
    1.11 +        length (type_args_named_constrained_of spec), mixfix_of spec);
    1.12  
    1.13 -    val fake_thy =
    1.14 -      Theory.copy #> fold (fn spec => fn thy =>
    1.15 -          case try (add_fake_type spec (mixfix_of spec)) thy of
    1.16 -            SOME thy' => thy'
    1.17 -          | NONE => add_fake_type spec Mixfix.NoSyn thy)
    1.18 -        specs;
    1.19 +    val fake_thy = Theory.copy #> fold add_fake_type specs;
    1.20      val fake_lthy = Proof_Context.background_theory fake_thy no_defs_lthy;
    1.21  
    1.22      fun mk_fake_T b =