src/Pure/Syntax/syntax.ML
changeset 24341 7b8da2396c49
parent 24278 cf82c471f9ee
child 24372 743575ccfec8
     1.1 --- a/src/Pure/Syntax/syntax.ML	Mon Aug 20 17:46:31 2007 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Aug 20 17:46:32 2007 +0200
     1.3 @@ -622,16 +622,16 @@
     1.4  
     1.5  fun type_check ts0 ctxt0 =
     1.6    let
     1.7 -    val funs = rev (TypeCheck.get (Context.Proof ctxt0));
     1.8 +    val funs = map #1 (rev (TypeCheck.get (Context.Proof ctxt0)));
     1.9      fun check [] ts ctxt = (ts, ctxt)
    1.10 -      | check ((f, _) :: fs) ts ctxt = f ts ctxt |-> check fs;
    1.11 +      | check (f :: fs) ts ctxt = f ts ctxt |-> check fs;
    1.12  
    1.13      fun check_fixpoint ts ctxt =
    1.14        let val (ts', ctxt') = check funs ts ctxt in
    1.15          if eq_list (op aconv) (ts, ts') then (ts, ctxt)
    1.16          else check_fixpoint ts' ctxt'
    1.17        end;
    1.18 -  in check_fixpoint ts0 ctxt0 end;
    1.19 +  in (case funs of [f] => f ts0 ctxt0 | _ => check_fixpoint ts0 ctxt0) end;
    1.20  
    1.21  fun check_terms ctxt ts = #1 (type_check ts ctxt);
    1.22  fun check_props ctxt = map (fn t => TypeInfer.constrain t propT) #> check_terms ctxt;