src/HOL/UNITY/Union.ML
changeset 11467 1064effe37f6
parent 10064 1a77667b21ef
child 11701 3d51fbf81c17
     1.1 --- a/src/HOL/UNITY/Union.ML	Mon Aug 06 15:54:29 2001 +0200
     1.2 +++ b/src/HOL/UNITY/Union.ML	Mon Aug 06 16:43:40 2001 +0200
     1.3 @@ -352,7 +352,7 @@
     1.4  
     1.5  bind_thm ("ok_sym", ok_commute RS iffD1);
     1.6  
     1.7 -Goal "OK {(0,F),(1,G),(2,H)} snd = (F ok G & (F Join G) ok H)";
     1.8 +Goal "OK {(#0::int,F),(#1,G),(#2,H)} snd = (F ok G & (F Join G) ok H)";
     1.9  by (asm_full_simp_tac
    1.10      (simpset() addsimps [Ball_def, conj_disj_distribR, ok_def, Join_def, 
    1.11                     OK_def, insert_absorb, all_conj_distrib, eq_commute]) 1);