1.1 --- a/src/HOL/Tools/datatype_case.ML	Mon Oct 08 22:06:32 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_case.ML	Tue Oct 09 00:20:13 2007 +0200
     1.3 @@ -247,7 +247,7 @@
     1.4                  in (pat_rect1, tree)
     1.5                  end)
     1.6              | SOME (t, i) => raise CASE_ERROR ("Not a datatype constructor: " ^
     1.7 -                ProofContext.string_of_term ctxt t, i)
     1.8 +                Syntax.string_of_term ctxt t, i)
     1.9            end
    1.10        | mk _ = raise CASE_ERROR ("Malformed row matrix", ~1)
    1.11    in mk
    1.12 @@ -260,13 +260,13 @@
    1.13    (fn x as Free (s, _) => (fn xs =>
    1.14          if member op aconv xs x then
    1.15            case_error (quote s ^ " occurs repeatedly in the pattern " ^
    1.16 -            quote (ProofContext.string_of_term ctxt pat))
    1.17 +            quote (Syntax.string_of_term ctxt pat))
    1.18          else x :: xs)
    1.19      | _ => I) pat [];
    1.20  
    1.21  fun gen_make_case ty_match ty_inst type_of tab ctxt err used x clauses =
    1.22    let
    1.23 -    fun string_of_clause (pat, rhs) = ProofContext.string_of_term ctxt
    1.24 +    fun string_of_clause (pat, rhs) = Syntax.string_of_term ctxt
    1.25        (Syntax.const "_case1" $ pat $ rhs);
    1.26      val _ = map (no_repeat_vars ctxt o fst) clauses;
    1.27      val rows = map_index (fn (i, (pat, rhs)) =>
    1.28 @@ -333,8 +333,7 @@
    1.29              in
    1.30                (t' $ u', used'')
    1.31              end
    1.32 -        | prep_pat t used = case_error ("Bad pattern: " ^
    1.33 -            ProofContext.string_of_term ctxt t);
    1.34 +        | prep_pat t used = case_error ("Bad pattern: " ^ Syntax.string_of_term ctxt t);
    1.35        fun dest_case1 (t as Const ("_case1", _) $ l $ r) =
    1.36              let val (l', cnstrts) = strip_constraints l
    1.37              in ((fst (prep_pat l' (add_term_free_names (t, []))), r), cnstrts)