# HG changeset patch # User webertj # Date 1167920984 -3600 # Node ID 337990f42ce0a4fc6006653effd7115b45cde6b8 # Parent 04528ce9ded58959c9768dbf3cd48f142c0f09c5 obsolete sign_of calls removed diff -r 04528ce9ded5 -r 337990f42ce0 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Thu Jan 04 14:01:41 2007 +0100 +++ b/src/HOL/Tools/refute.ML Thu Jan 04 15:29:44 2007 +0100 @@ -210,7 +210,7 @@ fun interpret thy model args t = (case get_first (fn (_, f) => f thy model args t) (#interpreters (RefuteData.get thy)) of - NONE => raise REFUTE ("interpret", "no interpreter for term " ^ quote (Sign.string_of_term (sign_of thy) t)) + NONE => raise REFUTE ("interpret", "no interpreter for term " ^ quote (Sign.string_of_term thy t)) | SOME x => x); (* ------------------------------------------------------------------------- *) @@ -222,7 +222,7 @@ fun print thy model t intr assignment = (case get_first (fn (_, f) => f thy model t intr assignment) (#printers (RefuteData.get thy)) of - NONE => raise REFUTE ("print", "no printer for term " ^ quote (Sign.string_of_term (sign_of thy) t)) + NONE => raise REFUTE ("print", "no printer for term " ^ quote (Sign.string_of_term thy t)) | SOME x => x); (* ------------------------------------------------------------------------- *) @@ -240,7 +240,7 @@ if null typs then "empty universe (no type variables in term)\n" else - "Size of types: " ^ commas (map (fn (T, i) => Sign.string_of_typ (sign_of thy) T ^ ": " ^ string_of_int i) typs) ^ "\n" + "Size of types: " ^ commas (map (fn (T, i) => Sign.string_of_typ thy T ^ ": " ^ string_of_int i) typs) ^ "\n" val show_consts_msg = if not (!show_consts) andalso Library.exists (is_Const o fst) terms then "set \"show_consts\" to show the interpretation of constants\n" @@ -253,7 +253,7 @@ space_implode "\n" (List.mapPartial (fn (t, intr) => (* print constants only if 'show_consts' is true *) if (!show_consts) orelse not (is_Const t) then - SOME (Sign.string_of_term (sign_of thy) t ^ ": " ^ Sign.string_of_term (sign_of thy) (print thy model t intr assignment)) + SOME (Sign.string_of_term thy t ^ ": " ^ Sign.string_of_term thy (print thy model t intr assignment)) else NONE) terms) ^ "\n" in @@ -916,7 +916,7 @@ val _ = (if Library.exists (fn d => case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps then - raise REFUTE ("ground_types", "datatype argument (for type " ^ Sign.string_of_typ (sign_of thy) (Type (s, Ts)) ^ ") is not a variable") + raise REFUTE ("ground_types", "datatype argument (for type " ^ Sign.string_of_typ thy (Type (s, Ts)) ^ ") is not a variable") else ()) (* if the current type is a recursive IDT (i.e. a depth is required), add it to 'acc' *) @@ -1065,13 +1065,13 @@ fun wrapper () = let val u = unfold_defs thy t - val _ = writeln ("Unfolded term: " ^ Sign.string_of_term (sign_of thy) u) + val _ = writeln ("Unfolded term: " ^ Sign.string_of_term thy u) val axioms = collect_axioms thy u (* Term.typ list *) val types = Library.foldl (fn (acc, t') => acc union (ground_types thy t')) ([], u :: axioms) val _ = writeln ("Ground types: " ^ (if null types then "none." - else commas (map (Sign.string_of_typ (sign_of thy)) types))) + else commas (map (Sign.string_of_typ thy) types))) (* we can only consider fragments of recursive IDTs, so we issue a *) (* warning if the formula contains a recursive IDT *) (* TODO: no warning needed for /positive/ occurrences of IDTs *) @@ -1143,7 +1143,7 @@ assert (maxtime>=0) ("\"maxtime\" is " ^ string_of_int maxtime ^ ", must be at least 0"); (* enter loop with or without time limit *) writeln ("Trying to find a model that " ^ (if negate then "refutes" else "satisfies") ^ ": " - ^ Sign.string_of_term (sign_of thy) t); + ^ Sign.string_of_term thy t); if maxtime>0 then ( interrupt_timeout (Time.fromSeconds (Int.toLarge maxtime)) wrapper () @@ -1847,7 +1847,7 @@ val _ = (if Library.exists (fn d => case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps then - raise REFUTE ("IDT_interpreter", "datatype argument (for type " ^ Sign.string_of_typ (sign_of thy) (Type (s, Ts)) ^ ") is not a variable") + raise REFUTE ("IDT_interpreter", "datatype argument (for type " ^ Sign.string_of_typ thy (Type (s, Ts)) ^ ") is not a variable") else ()) (* if the model specifies a depth for the current type, decrement it to avoid infinite recursion *) @@ -1915,7 +1915,7 @@ val _ = (if Library.exists (fn d => case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps then - raise REFUTE ("IDT_constructor_interpreter", "datatype argument (for type " ^ Sign.string_of_typ (sign_of thy) (Type (s', Ts')) ^ ") is not a variable") + raise REFUTE ("IDT_constructor_interpreter", "datatype argument (for type " ^ Sign.string_of_typ thy (Type (s', Ts')) ^ ") is not a variable") else ()) (* split the constructors into those occuring before/after 'Const (s, T)' *) @@ -2172,7 +2172,7 @@ let (* int * interpretation list -> int * int list *) fun get_cargs_rec (_, []) = - raise REFUTE ("IDT_recursion_interpreter", "no matching constructor found for element " ^ string_of_int elem ^ " in datatype " ^ Sign.string_of_typ (sign_of thy) IDT ^ " (datatype index " ^ string_of_int idx ^ ")") + raise REFUTE ("IDT_recursion_interpreter", "no matching constructor found for element " ^ string_of_int elem ^ " in datatype " ^ Sign.string_of_typ thy IDT ^ " (datatype index " ^ string_of_int idx ^ ")") | get_cargs_rec (n, x::xs) = (case get_args x elem of SOME args => (n, args) @@ -2744,7 +2744,7 @@ val _ = (if Library.exists (fn d => case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps then - raise REFUTE ("IDT_printer", "datatype argument (for type " ^ Sign.string_of_typ (sign_of thy) (Type (s, Ts)) ^ ") is not a variable") + raise REFUTE ("IDT_printer", "datatype argument (for type " ^ Sign.string_of_typ thy (Type (s, Ts)) ^ ") is not a variable") else ()) (* the index of the element in the datatype *)