Mercurialisabelle / changeset
summary | shortlog | changelog | graph | tags | branches | files | changeset | raw | gz
ProofContext.inferred_param;
authorwenzelm
Tue Jan 24 00:43:32 2006 +0100 (2006-01-24)
changeset 18769e90eb0bc0ddd
parent 18768 6e97b57cdcba
child 18770 434f660d3068
ProofContext.inferred_param;
src/Pure/Isar/obtain.ML file | annotate | diff | revisions 
     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 =
isabelle