Fixed bug in simpdata.ML that prevented the use of congruence rules from a
authorballarin
Mon Dec 09 10:38:56 2002 +0100 (2002-12-09)
changeset 13743f8f9393be64c
parent 13742 452ff5d0b69d
child 13744 2241191a3c54
Fixed bug in simpdata.ML that prevented the use of congruence rules from a
locale. (mk_meta_cong did wrongly convert metahyps to hyps)
src/HOL/hologic.ML
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/hologic.ML	Fri Dec 06 15:16:30 2002 +0100
     1.2 +++ b/src/HOL/hologic.ML	Mon Dec 09 10:38:56 2002 +0100
     1.3 @@ -159,7 +159,7 @@
     1.4  fun mk_UNIV T = Const ("UNIV", mk_setT T);
     1.5  
     1.6  
     1.7 -(* binary oprations and relations *)
     1.8 +(* binary operations and relations *)
     1.9  
    1.10  fun mk_binop c (t, u) =
    1.11    let val T = fastype_of t in
    1.12 @@ -280,7 +280,7 @@
    1.13  
    1.14  val binT = Type ("Numeral.bin", []);
    1.15  
    1.16 -val pls_const =  Const ("Numeral.bin.Pls", binT)
    1.17 +val pls_const = Const ("Numeral.bin.Pls", binT)
    1.18  and min_const = Const ("Numeral.bin.Min", binT)
    1.19  and bit_const = Const ("Numeral.bin.Bit", [binT, boolT] ---> binT);
    1.20  
     2.1 --- a/src/HOL/simpdata.ML	Fri Dec 06 15:16:30 2002 +0100
     2.2 +++ b/src/HOL/simpdata.ML	Mon Dec 09 10:38:56 2002 +0100
     2.3 @@ -151,7 +151,7 @@
     2.4  
     2.5  (*Congruence rules for = (instead of ==)*)
     2.6  fun mk_meta_cong rl =
     2.7 -  standard(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
     2.8 +  zero_var_indexes(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
     2.9    handle THM _ =>
    2.10    error("Premises and conclusion of congruence rules must be =-equalities");
    2.11