# HG changeset patch
# User wenzelm
# Date 1164310421 -3600
# Node ID 146938537ddc26d519e8e6c3de369a1b89493941
# Parent  fbd6422a847adc86ff1b3c3797826f1039b3d4f6
renamed Args.Name to Args.Text;

diff -r fbd6422a847a -r 146938537ddc src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Thu Nov 23 20:33:39 2006 +0100
+++ b/src/Pure/Isar/rule_insts.ML	Thu Nov 23 20:33:41 2006 +0100
@@ -66,10 +66,10 @@
     val (type_insts, term_insts) = List.partition (is_tvar o fst) mixed_insts;
     val internal_insts = term_insts |> map_filter
       (fn (xi, Args.Term t) => SOME (xi, t)
-        | (_, Args.Name _) => NONE
+        | (_, Args.Text _) => NONE
         | (xi, _) => error_var "Term argument expected for " xi);
     val external_insts = term_insts |> map_filter
-      (fn (xi, Args.Name s) => SOME (xi, s) | _ => NONE);
+      (fn (xi, Args.Text s) => SOME (xi, s) | _ => NONE);
 
 
     (* mixed type instantiations *)
@@ -79,7 +79,7 @@
         val S = the_sort tvars xi;
         val T =
           (case arg of
-            Args.Name s => ProofContext.read_typ ctxt s
+            Args.Text s => ProofContext.read_typ ctxt s
           | Args.Typ T => T
           | _ => error_var "Type argument expected for " xi);
       in
@@ -169,7 +169,7 @@
 val value =
   Args.internal_typ >> Args.Typ ||
   Args.internal_term >> Args.Term ||
-  Args.name >> Args.Name;
+  Args.name >> Args.Text;
 
 val inst = Args.var -- (Args.$$$ "=" |-- Args.ahead -- value)
   >> (fn (xi, (a, v)) => (a, (xi, v)));
@@ -188,7 +188,7 @@
 
 val value =
   Args.internal_term >> Args.Term ||
-  Args.name >> Args.Name;
+  Args.name >> Args.Text;
 
 val inst = Args.ahead -- Args.maybe value;
 val concl = Args.$$$ "concl" -- Args.colon;