# HG changeset patch
# User wenzelm
# Date 951404384 -3600
# Node ID 93e125b212206b7eab29ca0445c7e9fdbd6c0daf
# Parent  5469b894f30b594490d723ed5b372223612d13c6
workaround res_inst_tac/lift_inst_rule bug by explicit type contraint;

diff -r 5469b894f30b -r 93e125b21220 src/HOL/Univ.ML
--- 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);