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");