1.1 --- a/src/ZF/Tools/typechk.ML	Wed Jun 29 20:39:41 2011 +0200
     1.2 +++ b/src/ZF/Tools/typechk.ML	Wed Jun 29 21:34:16 2011 +0200
     1.3 @@ -107,7 +107,7 @@
     1.4  
     1.5  val type_solver =
     1.6    Simplifier.mk_solver "ZF typecheck" (fn ss =>
     1.7 -    type_solver_tac (Simplifier.the_context ss) (prems_of_ss ss));
     1.8 +    type_solver_tac (Simplifier.the_context ss) (Simplifier.prems_of ss));
     1.9  
    1.10  
    1.11  (* concrete syntax *)