src/HOL/Tools/inductive_package.ML
changeset 24920 2a45e400fdad
parent 24915 fc90277c0dd7
child 24925 f38dd8d0a30d
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Mon Oct 08 22:06:32 2007 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Oct 09 00:20:13 2007 +0200
     1.3 @@ -247,11 +247,11 @@
     1.4  
     1.5  fun err_in_rule ctxt name t msg =
     1.6    error (cat_lines ["Ill-formed introduction rule " ^ quote name,
     1.7 -    ProofContext.string_of_term ctxt t, msg]);
     1.8 +    Syntax.string_of_term ctxt t, msg]);
     1.9  
    1.10  fun err_in_prem ctxt name t p msg =
    1.11 -  error (cat_lines ["Ill-formed premise", ProofContext.string_of_term ctxt p,
    1.12 -    "in introduction rule " ^ quote name, ProofContext.string_of_term ctxt t, msg]);
    1.13 +  error (cat_lines ["Ill-formed premise", Syntax.string_of_term ctxt p,
    1.14 +    "in introduction rule " ^ quote name, Syntax.string_of_term ctxt t, msg]);
    1.15  
    1.16  val bad_concl = "Conclusion of introduction rule must be an inductive predicate";
    1.17  
    1.18 @@ -275,7 +275,7 @@
    1.19  
    1.20      fun check_ind err t = case dest_predicate cs params t of
    1.21          NONE => err (bad_app ^
    1.22 -          commas (map (ProofContext.string_of_term ctxt) params))
    1.23 +          commas (map (Syntax.string_of_term ctxt) params))
    1.24        | SOME (_, _, ys, _) =>
    1.25            if exists (fn c => exists (fn t => Logic.occs (c, t)) ys) cs
    1.26            then err bad_ind_occ else ();
    1.27 @@ -431,7 +431,7 @@
    1.28  
    1.29      fun err msg =
    1.30        error (Pretty.string_of (Pretty.block
    1.31 -        [Pretty.str msg, Pretty.fbrk, ProofContext.pretty_term ctxt prop]));
    1.32 +        [Pretty.str msg, Pretty.fbrk, Syntax.pretty_term ctxt prop]));
    1.33  
    1.34      val elims = Induct.find_casesP ctxt prop;
    1.35