1.1 --- a/src/HOL/Tools/function_package/lexicographic_order.ML	Mon Oct 08 22:06:32 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Tue Oct 09 00:20:13 2007 +0200
     1.3 @@ -252,7 +252,7 @@
     1.4  
     1.5  fun no_order_msg ctxt table tl measure_funs =
     1.6      let
     1.7 -      val prterm = ProofContext.string_of_term ctxt
     1.8 +      val prterm = Syntax.string_of_term ctxt
     1.9        fun pr_fun t i = string_of_int i ^ ") " ^ prterm t
    1.10  
    1.11        fun pr_goal t i =
    1.12 @@ -292,7 +292,7 @@
    1.13        val clean_table = map (fn x => map (nth x) order) table
    1.14  
    1.15        val relation = mk_measures domT (map (nth measure_funs) order)
    1.16 -      val _ = writeln ("Found termination order: " ^ quote (ProofContext.string_of_term ctxt relation))
    1.17 +      val _ = writeln ("Found termination order: " ^ quote (Syntax.string_of_term ctxt relation))
    1.18  
    1.19      in (* 4: proof reconstruction *)
    1.20        st |> (PRIMITIVE (cterm_instantiate [(cterm_of thy rel, cterm_of thy relation)])