src/HOL/simpdata.ML
changeset 16587 b34c8aa657a5
parent 15570 8d8c70b41bab
child 16633 208ebc9311f2
     1.1 --- a/src/HOL/simpdata.ML	Tue Jun 28 15:26:45 2005 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Tue Jun 28 15:27:45 2005 +0200
     1.3 @@ -240,7 +240,7 @@
     1.4  val mksimps_pairs =
     1.5    [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
     1.6     ("All", [spec]), ("True", []), ("False", []),
     1.7 -   ("If", [if_bool_eq_conj RS iffD1])];
     1.8 +   ("HOL.If", [if_bool_eq_conj RS iffD1])];
     1.9  
    1.10  (*
    1.11  val mk_atomize:      (string * thm list) list -> thm -> thm list