src/HOL/Tools/refute.ML

 
   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 thy t))
+        "no interpreter for term " ^ quote (Syntax.string_of_term_global thy t))
     | SOME x => x;
 
 (* ------------------------------------------------------------------------- *)
 (* print: converts the interpretation 'intr', which must denote a term of    *)
 (*        type 'T', into a term using a suitable printer                     *)

 
   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 type " ^ quote (Sign.string_of_typ thy T))
+        "no printer for type " ^ quote (Syntax.string_of_typ_global thy T))
     | SOME x => x;
 
 (* ------------------------------------------------------------------------- *)
 (* print_model: turns the model into a string, using a fixed interpretation  *)
 (*              (given by an assignment for Boolean variables) and suitable  *)

     val typs_msg =
       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 thy T ^ ": " ^ string_of_int i) typs) ^ "\n"
+          Syntax.string_of_typ_global 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"
       else
         ""

         "empty interpretation (no free variables in term)\n"
       else
         cat_lines (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 thy t ^ ": " ^
-              Sign.string_of_term thy
+            SOME (Syntax.string_of_term_global thy t ^ ": " ^
+              Syntax.string_of_term_global thy
                 (print thy model (Term.type_of t) intr assignment))
           else
             NONE) terms) ^ "\n"
   in
     typs_msg ^ show_consts_msg ^ terms_msg

         case Type.lookup typeSubs v of
           NONE =>
           (* schematic type variable not instantiated *)
           raise REFUTE ("monomorphic_term",
             "no substitution for type variable " ^ fst (fst v) ^
-            " in term " ^ Sign.string_of_term CPure.thy t)
+            " in term " ^ Syntax.string_of_term_global CPure.thy t)
         | SOME typ =>
           typ)) t;
 
 (* ------------------------------------------------------------------------- *)
 (* specialize_type: given a constant 's' of type 'T', which is a subterm of  *)

       (* string list *)
       val sort = (case T of
           TFree (_, sort) => sort
         | TVar (_, sort)  => sort
         | _               => raise REFUTE ("collect_axioms", "type " ^
-          Sign.string_of_typ thy T ^ " is not a variable"))
+          Syntax.string_of_typ_global thy T ^ " is not a variable"))
       (* obtain axioms for all superclasses *)
       val superclasses = sort @ (maps (Sign.super_classes thy) sort)
       (* merely an optimization, because 'collect_this_axiom' disallows *)
       (* duplicate axioms anyway:                                       *)
       val superclasses = distinct (op =) superclasses

           (axname, ax)
         | [(idx, S)] =>
           (axname, monomorphic_term (Vartab.make [(idx, (S, T))]) ax)
         | _ =>
           raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^
-            Sign.string_of_term thy ax ^
+            Syntax.string_of_term_global thy ax ^
             ") contains more than one type variable")))
         class_axioms
     in
       fold collect_this_axiom monomorphic_class_axioms axs
     end

               val class   = Logic.class_of_const s
               val inclass = Logic.mk_inclass (TVar (("'a", 0), [class]), class)
               val ax_in   = SOME (specialize_type thy (s, T) inclass)
                 (* type match may fail due to sort constraints *)
                 handle Type.TYPE_MATCH => NONE
-              val ax_1 = Option.map (fn ax => (Sign.string_of_term thy ax, ax))
+              val ax_1 = Option.map (fn ax => (Syntax.string_of_term_global thy ax, ax))
                 ax_in
               val ax_2 = Option.map (apsnd (specialize_type thy (s, T)))
                 (get_classdef thy class)
             in
               collect_type_axioms (fold collect_this_axiom

             (* sanity check: every element in 'dtyps' must be a *)
             (* 'DtTFree'                                        *)
             val _ = if Library.exists (fn d =>
               case d of DatatypeAux.DtTFree _ => false | _ => true) typs then
               raise REFUTE ("ground_types", "datatype argument (for type "
-                ^ Sign.string_of_typ thy T ^ ") is not a variable")
+                ^ Syntax.string_of_typ_global thy T ^ ") is not a variable")
             else ()
             (* required for mutually recursive datatypes; those need to   *)
             (* be added even if they are an instance of an otherwise non- *)
             (* recursive datatype                                         *)
             fun collect_dtyp (d, acc) =

   let
     (* unit -> unit *)
     fun wrapper () =
     let
       val u      = unfold_defs thy t
-      val _      = writeln ("Unfolded term: " ^ Sign.string_of_term thy u)
+      val _      = writeln ("Unfolded term: " ^ Syntax.string_of_term_global 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 thy) types)))
+           else commas (map (Syntax.string_of_typ_global 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       *)
       val _ = if Library.exists (fn
           Type (s, _) =>

       maxtime>=0 orelse
         error ("\"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 thy t);
+        ^ Syntax.string_of_term_global thy t);
       if maxtime>0 then (
         TimeLimit.timeLimit (Time.fromSeconds maxtime)
           wrapper ()
         handle TimeLimit.TimeOut =>
           writeln ("\nSearch terminated, time limit (" ^ string_of_int maxtime

               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 thy (Type (s, Ts))
+                    ^ Syntax.string_of_typ_global 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             *)
               val typs'    = case depth of NONE => typs | SOME n =>

               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 thy T
+                    ^ Syntax.string_of_typ_global thy T
                     ^ ") is not a variable")
                 else ()
               (* decrement depth for the IDT 'T' *)
               val typs' = (case AList.lookup (op =) typs T of NONE => typs
                 | SOME n => AList.update (op =) (T, n-1) typs)

               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 thy (Type (s', Ts'))
+                    ^ Syntax.string_of_typ_global thy (Type (s', Ts'))
                     ^ ") is not a variable")
                 else ()
               (* split the constructors into those occuring before/after *)
               (* 'Const (s, T)'                                          *)
               val (constrs1, constrs2) = take_prefix (fn (cname, ctypes) =>

           (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
           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 thy (Type (s, Ts)) ^ ") is not a variable")
+                Syntax.string_of_typ_global thy (Type (s, Ts)) ^ ") is not a variable")
             else ()
           (* the index of the element in the datatype *)
           val element = (case intr of
               Leaf xs => find_index (PropLogic.eval assignment) xs
             | Node _  => raise REFUTE ("IDT_printer",