src/HOL/Univ.ML
changeset 8292 93e125b21220
parent 8114 09a7a180cc99
child 8703 816d8f6513be
--- a/src/HOL/Univ.ML	Thu Feb 24 15:58:10 2000 +0100
+++ b/src/HOL/Univ.ML	Thu Feb 24 15:59:44 2000 +0100
@@ -425,7 +425,7 @@
 
 val [p1, p2] = Goalw [o_def]
      "[| f : Funs (range g); !!h. f = g o h ==> P |] ==> P";
-by (res_inst_tac [("h", "%x. @y. f x = g y")] p2 1);
+by (res_inst_tac [("h", "%x. @y. (f::'a=>'b) x = g y")] p2 1);
 by (rtac ext 1);
 by (rtac (p1 RS FunsD RS rangeE) 1);
 by (etac (exI RS (select_eq_Ex RS iffD2)) 1);