src/Pure/Isar/obtain.ML
changeset 18769 e90eb0bc0ddd
parent 18728 6790126ab5f6
child 18870 020e242c02a0
     1.1 --- a/src/Pure/Isar/obtain.ML	Tue Jan 24 00:43:31 2006 +0100
     1.2 +++ b/src/Pure/Isar/obtain.ML	Tue Jan 24 00:43:32 2006 +0100
     1.3 @@ -199,7 +199,7 @@
     1.4    in (xs' @ ys', rule') end;
     1.5  
     1.6  fun inferred_type (x, _, mx) ctxt =
     1.7 -  let val ((_, T), ctxt') = ProofContext.inferred_type x ctxt
     1.8 +  let val ((_, T), ctxt') = ProofContext.inferred_param x ctxt
     1.9    in ((x, SOME T, mx), ctxt') end;
    1.10  
    1.11  fun gen_guess prep_vars raw_vars int state =