| changeset 3842 | b55686a7b22c |
| parent 3018 | e65b60b28341 |
| child 3919 | c036caebfc75 |
--- a/src/HOL/MiniML/Instance.ML Fri Oct 10 18:37:49 1997 +0200 +++ b/src/HOL/MiniML/Instance.ML Fri Oct 10 19:02:28 1997 +0200 @@ -211,7 +211,7 @@ goalw thy [le_type_scheme_def,is_bound_typ_instance] "sch <= BVar n"; by (strip_tac 1); -by (res_inst_tac [("x","%a.t")]exI 1); +by (res_inst_tac [("x","%a. t")]exI 1); by (Simp_tac 1); qed "bound_typ_instance_BVar"; AddIffs [bound_typ_instance_BVar];