1.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Mon Oct 08 22:06:32 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Tue Oct 09 00:20:13 2007 +0200
     1.3 @@ -175,7 +175,7 @@
     1.4  
     1.5  fun split_def ctxt geq =
     1.6      let
     1.7 -      fun input_error msg = cat_lines [msg, ProofContext.string_of_term ctxt geq]
     1.8 +      fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
     1.9        val (qs, imp) = open_all_all geq
    1.10  
    1.11        val gs = Logic.strip_imp_prems imp
    1.12 @@ -214,7 +214,7 @@
    1.13                                  
    1.14        fun check geq = 
    1.15            let
    1.16 -            fun input_error msg = cat_lines [msg, ProofContext.string_of_term ctxt geq]
    1.17 +            fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
    1.18                                    
    1.19              val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq
    1.20