# HG changeset patch
# User wenzelm
# Date 1138059812 -3600
# Node ID e90eb0bc0dddbb6c59796cd3b1c55c5465d6f59b
# Parent  6e97b57cdcba3a1f87fd7bd8fb1a31d23056239f
ProofContext.inferred_param;

diff -r 6e97b57cdcba -r e90eb0bc0ddd src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Tue Jan 24 00:43:31 2006 +0100
+++ b/src/Pure/Isar/obtain.ML	Tue Jan 24 00:43:32 2006 +0100
@@ -199,7 +199,7 @@
   in (xs' @ ys', rule') end;
 
 fun inferred_type (x, _, mx) ctxt =
-  let val ((_, T), ctxt') = ProofContext.inferred_type x ctxt
+  let val ((_, T), ctxt') = ProofContext.inferred_param x ctxt
   in ((x, SOME T, mx), ctxt') end;
 
 fun gen_guess prep_vars raw_vars int state =