diff -r 811f78424efc -r 7b8da2396c49 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Mon Aug 20 17:46:31 2007 +0200
+++ b/src/Pure/Syntax/syntax.ML	Mon Aug 20 17:46:32 2007 +0200
@@ -622,16 +622,16 @@
 
 fun type_check ts0 ctxt0 =
   let
-    val funs = rev (TypeCheck.get (Context.Proof ctxt0));
+    val funs = map #1 (rev (TypeCheck.get (Context.Proof ctxt0)));
     fun check [] ts ctxt = (ts, ctxt)
-      | check ((f, _) :: fs) ts ctxt = f ts ctxt |-> check fs;
+      | check (f :: fs) ts ctxt = f ts ctxt |-> check fs;
 
     fun check_fixpoint ts ctxt =
       let val (ts', ctxt') = check funs ts ctxt in
         if eq_list (op aconv) (ts, ts') then (ts, ctxt)
         else check_fixpoint ts' ctxt'
       end;
-  in check_fixpoint ts0 ctxt0 end;
+  in (case funs of [f] => f ts0 ctxt0 | _ => check_fixpoint ts0 ctxt0) end;
 
 fun check_terms ctxt ts = #1 (type_check ts ctxt);
 fun check_props ctxt = map (fn t => TypeInfer.constrain t propT) #> check_terms ctxt;