Fixed bug in simpdata.ML that prevented the use of congruence rules from a
locale. (mk_meta_cong did wrongly convert metahyps to hyps)
--- a/src/HOL/hologic.ML Fri Dec 06 15:16:30 2002 +0100
+++ b/src/HOL/hologic.ML Mon Dec 09 10:38:56 2002 +0100
@@ -159,7 +159,7 @@
fun mk_UNIV T = Const ("UNIV", mk_setT T);
-(* binary oprations and relations *)
+(* binary operations and relations *)
fun mk_binop c (t, u) =
let val T = fastype_of t in
@@ -280,7 +280,7 @@
val binT = Type ("Numeral.bin", []);
-val pls_const = Const ("Numeral.bin.Pls", binT)
+val pls_const = Const ("Numeral.bin.Pls", binT)
and min_const = Const ("Numeral.bin.Min", binT)
and bit_const = Const ("Numeral.bin.Bit", [binT, boolT] ---> binT);
--- a/src/HOL/simpdata.ML Fri Dec 06 15:16:30 2002 +0100
+++ b/src/HOL/simpdata.ML Mon Dec 09 10:38:56 2002 +0100
@@ -151,7 +151,7 @@
(*Congruence rules for = (instead of ==)*)
fun mk_meta_cong rl =
- standard(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
+ zero_var_indexes(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
handle THM _ =>
error("Premises and conclusion of congruence rules must be =-equalities");