src/Pure/sign.ML
changeset 42204 b3277168c1e7
parent 40959 49765c1104d4
child 42224 578a51fae383
     1.1 --- a/src/Pure/sign.ML	Sun Apr 03 18:17:21 2011 +0200
     1.2 +++ b/src/Pure/sign.ML	Sun Apr 03 21:59:33 2011 +0200
     1.3 @@ -108,10 +108,8 @@
     1.4      (string * string * (Proof.context -> string -> Pretty.T)) list -> theory -> theory
     1.5    val add_mode_tokentrfuns: string -> (string * (Proof.context -> string -> Pretty.T)) list
     1.6      -> theory -> theory
     1.7 -  val add_trrules: (xstring * string) Syntax.trrule list -> theory -> theory
     1.8 -  val del_trrules: (xstring * string) Syntax.trrule list -> theory -> theory
     1.9 -  val add_trrules_i: ast Syntax.trrule list -> theory -> theory
    1.10 -  val del_trrules_i: ast Syntax.trrule list -> theory -> theory
    1.11 +  val add_trrules: ast Syntax.trrule list -> theory -> theory
    1.12 +  val del_trrules: ast Syntax.trrule list -> theory -> theory
    1.13    val new_group: theory -> theory
    1.14    val reset_group: theory -> theory
    1.15    val add_path: string -> theory -> theory
    1.16 @@ -497,14 +495,8 @@
    1.17  
    1.18  (* translation rules *)
    1.19  
    1.20 -fun gen_trrules f args thy = thy |> map_syn (fn syn =>
    1.21 -  let val rules = map (Syntax.map_trrule (apfst (intern_type thy))) args
    1.22 -  in f (ProofContext.init_global thy) syn rules syn end);
    1.23 -
    1.24 -val add_trrules = gen_trrules Syntax.update_trrules;
    1.25 -val del_trrules = gen_trrules Syntax.remove_trrules;
    1.26 -val add_trrules_i = map_syn o Syntax.update_trrules_i;
    1.27 -val del_trrules_i = map_syn o Syntax.remove_trrules_i;
    1.28 +val add_trrules = map_syn o Syntax.update_trrules;
    1.29 +val del_trrules = map_syn o Syntax.remove_trrules;
    1.30  
    1.31  
    1.32  (* naming *)