Term.string_of_vname;
authorwenzelm
Sat Apr 14 17:36:05 2007 +0200 (2007-04-14)
changeset 2267823963361278c
parent 22677 b11a9beabe7d
child 22679 68cd69a388e2
Term.string_of_vname;
src/Provers/blast.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/proof_context.ML
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/envir.ML
src/Pure/pattern.ML
src/Pure/type_infer.ML
     1.1 --- a/src/Provers/blast.ML	Sat Apr 14 17:36:03 2007 +0200
     1.2 +++ b/src/Provers/blast.ML	Sat Apr 14 17:36:05 2007 +0200
     1.3 @@ -1212,7 +1212,7 @@
     1.4                       | SOME(v,is) => if is=bounds ts then Var v
     1.5                              else raise TRANS
     1.6                                  ("Discrepancy among occurrences of "
     1.7 -                                 ^ Syntax.string_of_vname ix))
     1.8 +                                 ^ Term.string_of_vname ix))
     1.9              | Term.Abs (a,_,body) =>
    1.10                    if null ts then Abs(a, from (lev+1) body)
    1.11                    else raise TRANS "argument not in normal form"
     2.1 --- a/src/Pure/Isar/locale.ML	Sat Apr 14 17:36:03 2007 +0200
     2.2 +++ b/src/Pure/Isar/locale.ML	Sat Apr 14 17:36:05 2007 +0200
     2.3 @@ -2133,7 +2133,7 @@
     2.4        |> fold Term.add_varnames all_vs
     2.5      val _ = if null vars then ()
     2.6           else error ("Illegal schematic variable(s) in instantiation: " ^
     2.7 -           commas_quote (map Syntax.string_of_vname vars));
     2.8 +           commas_quote (map Term.string_of_vname vars));
     2.9      (* replace new types (which are TFrees) by ones with new names *)
    2.10      val new_Tnames = map fst (fold Term.add_tfrees all_vs [])
    2.11        |> Name.names (Name.make_context used) "'a"
     3.1 --- a/src/Pure/Isar/proof_context.ML	Sat Apr 14 17:36:03 2007 +0200
     3.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Apr 14 17:36:05 2007 +0200
     3.3 @@ -460,7 +460,7 @@
     3.4    Consts.certify (pp ctxt) (tsig_of ctxt) (consts_of ctxt);
     3.5  
     3.6  fun reject_schematic (Var (xi, _)) =
     3.7 -      error ("Unbound schematic variable: " ^ Syntax.string_of_vname xi)
     3.8 +      error ("Unbound schematic variable: " ^ Term.string_of_vname xi)
     3.9    | reject_schematic (Abs (_, _, t)) = reject_schematic t
    3.10    | reject_schematic (t $ u) = (reject_schematic t; reject_schematic u)
    3.11    | reject_schematic _ = ();
     4.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Apr 14 17:36:03 2007 +0200
     4.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Apr 14 17:36:05 2007 +0200
     4.3 @@ -78,7 +78,7 @@
     4.4        (case try Name.dest_skolem x of
     4.5          NONE => tagit var_tag s
     4.6        | SOME x' => tagit skolem_tag
     4.7 -          (setmp show_question_marks true Syntax.string_of_vname (x', i)))
     4.8 +          (setmp show_question_marks true Term.string_of_vname (x', i)))
     4.9    | NONE => tagit var_tag s);
    4.10  
    4.11  val proof_general_trans =
     5.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Apr 14 17:36:03 2007 +0200
     5.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Apr 14 17:36:05 2007 +0200
     5.3 @@ -89,7 +89,7 @@
     5.4        (case try Name.dest_skolem x of
     5.5          NONE => tagit var_tag s
     5.6        | SOME x' => tagit skolem_tag
     5.7 -          (setmp show_question_marks true Syntax.string_of_vname (x', i)))
     5.8 +          (setmp show_question_marks true Term.string_of_vname (x', i)))
     5.9    | NONE => tagit var_tag s);
    5.10  
    5.11  val proof_general_trans =
     6.1 --- a/src/Pure/envir.ML	Sat Apr 14 17:36:03 2007 +0200
     6.2 +++ b/src/Pure/envir.ML	Sat Apr 14 17:36:05 2007 +0200
     6.3 @@ -74,7 +74,7 @@
     6.4    in  (env',v)  end;
     6.5  
     6.6  fun var_clash ixn T T' = raise TYPE ("Variable " ^
     6.7 -  quote (Syntax.string_of_vname ixn) ^ " has two distinct types",
     6.8 +  quote (Term.string_of_vname ixn) ^ " has two distinct types",
     6.9    [T', T], []);
    6.10  
    6.11  fun gen_lookup f asol (xname, T) =
     7.1 --- a/src/Pure/pattern.ML	Sat Apr 14 17:36:03 2007 +0200
     7.2 +++ b/src/Pure/pattern.ML	Sat Apr 14 17:36:05 2007 +0200
     7.3 @@ -71,7 +71,7 @@
     7.4  
     7.5  fun proj_fail thy (env,binders,F,_,is,t) =
     7.6    if !trace_unify_fail
     7.7 -  then let val f = Syntax.string_of_vname F
     7.8 +  then let val f = Term.string_of_vname F
     7.9             val xs = bnames binders is
    7.10             val u = string_of_term thy env binders t
    7.11             val ys = bnames binders (subtract (op =) is (loose_bnos t))
    7.12 @@ -83,7 +83,7 @@
    7.13  
    7.14  fun ocheck_fail thy (F,t,binders,env) =
    7.15    if !trace_unify_fail
    7.16 -  then let val f = Syntax.string_of_vname F
    7.17 +  then let val f = Term.string_of_vname F
    7.18             val u = string_of_term thy env binders t
    7.19         in tracing("Variable " ^ f ^ " occurs in term\n" ^ u ^
    7.20                    "\nCannot unify!\n")
     8.1 --- a/src/Pure/type_infer.ML	Sat Apr 14 17:36:03 2007 +0200
     8.2 +++ b/src/Pure/type_infer.ML	Sat Apr 14 17:36:05 2007 +0200
     8.3 @@ -273,7 +273,7 @@
     8.4            else raise NO_UNIFIER (not_of_sort x S' S)
     8.5        | meet (PTVar (xi, S'), S) =
     8.6            if Type.subsort tsig (S', S) then ()
     8.7 -          else raise NO_UNIFIER (not_of_sort (Syntax.string_of_vname xi) S' S)
     8.8 +          else raise NO_UNIFIER (not_of_sort (Term.string_of_vname xi) S' S)
     8.9        | meet (Param _, _) = sys_error "meet";
    8.10  
    8.11  
    8.12 @@ -456,7 +456,7 @@
    8.13      val env = distinct eq (map (apsnd map_sort) raw_env);
    8.14      val _ = (case duplicates (eq_fst (op =)) env of [] => ()
    8.15        | dups => error ("Inconsistent sort constraints for type variable(s) "
    8.16 -          ^ commas_quote (map (Syntax.string_of_vname' o fst) dups)));
    8.17 +          ^ commas_quote (map (Term.string_of_vname' o fst) dups)));
    8.18  
    8.19      fun get xi =
    8.20        (case (AList.lookup (op =) env xi, def_sort xi) of
    8.21 @@ -466,7 +466,7 @@
    8.22        | (SOME S, SOME S') =>
    8.23            if Type.eq_sort tsig (S, S') then S'
    8.24            else error ("Sort constraint inconsistent with default for type variable " ^
    8.25 -            quote (Syntax.string_of_vname' xi)));
    8.26 +            quote (Term.string_of_vname' xi)));
    8.27    in get end;
    8.28  
    8.29