src/Tools/Code/code_target.ML
changeset 37844 f26becedaeb1
parent 37840 a3632a0b7d6c
child 37863 7f113caabcf4
child 37876 48116a1764c5
     1.1 --- a/src/Tools/Code/code_target.ML	Fri Jul 16 13:58:37 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Fri Jul 16 14:11:08 2010 +0200
     1.3 @@ -425,32 +425,32 @@
     1.4  fun read_inst thy (raw_tyco, raw_class) =
     1.5    (read_class thy raw_class, read_tyco thy raw_tyco);
     1.6  
     1.7 -fun gen_add_syntax (mapp, upd, del) prep_x prep_syn check target raw_x some_raw_syn thy =
     1.8 +fun gen_add_syntax (mapp, upd, del) prep_x prep_syn target raw_x some_raw_syn thy =
     1.9    let
    1.10      val x = prep_x thy raw_x;
    1.11 -    fun make_syn raw_syn = (check thy x raw_syn: unit; prep_syn raw_syn);
    1.12 -  in case some_raw_syn
    1.13 -   of SOME raw_syn => (map_name_syntax target o mapp) (upd (x, make_syn raw_syn)) thy
    1.14 -    | NONE => (map_name_syntax target o mapp) (del x) thy
    1.15 -  end;
    1.16 +    val change = case some_raw_syn
    1.17 +     of SOME raw_syn => upd (x, prep_syn thy x raw_syn)
    1.18 +      | NONE => del x;
    1.19 +  in (map_name_syntax target o mapp) change thy end;
    1.20  
    1.21  fun gen_add_syntax_class prep_class =
    1.22 -  gen_add_syntax (apfst o apfst, Symtab.update, Symtab.delete_safe) prep_class I ((K o K o K) ());
    1.23 +  gen_add_syntax (apfst o apfst, Symtab.update, Symtab.delete_safe) prep_class ((K o K) I);
    1.24  
    1.25  fun gen_add_syntax_inst prep_inst =
    1.26 -  gen_add_syntax (apfst o apsnd, Symreltab.update, Symreltab.delete_safe) prep_inst I ((K o K o K) ());
    1.27 +  gen_add_syntax (apfst o apsnd, Symreltab.update, Symreltab.delete_safe) prep_inst ((K o K) I);
    1.28  
    1.29  fun gen_add_syntax_tyco prep_tyco =
    1.30 -  gen_add_syntax (apsnd o apfst, Symtab.update, Symtab.delete_safe) prep_tyco I
    1.31 -    (fn thy => fn tyco => fn (n, _) => if n <> Sign.arity_number thy tyco
    1.32 +  gen_add_syntax (apsnd o apfst, Symtab.update, Symtab.delete_safe) prep_tyco
    1.33 +    (fn thy => fn tyco => fn syn => if fst syn <> Sign.arity_number thy tyco
    1.34        then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
    1.35 -      else ());
    1.36 +      else syn);
    1.37  
    1.38 -fun gen_add_syntax_const prep_const prep_syn check_raw_syn =
    1.39 -  gen_add_syntax (apsnd o apsnd, Symtab.update, Symtab.delete_safe) prep_const prep_syn
    1.40 -    (fn thy => fn c => fn (n, _) => if n > Code.args_number thy c
    1.41 +fun gen_add_syntax_const prep_const prep_syn =
    1.42 +  gen_add_syntax (apsnd o apsnd, Symtab.update, Symtab.delete_safe) prep_const
    1.43 +    (fn thy => fn c => fn raw_syn => let val syn = prep_syn raw_syn in
    1.44 +      if fst syn > Code.args_number thy c
    1.45        then error ("Too many arguments in syntax for constant " ^ quote c)
    1.46 -      else ()) check_raw_syn;
    1.47 +      else syn end);
    1.48  
    1.49  fun add_reserved target =
    1.50    let