renamed Args.Name to Args.Text;
authorwenzelm
Thu Nov 23 20:33:41 2006 +0100 (2006-11-23)
changeset 21500146938537ddc
parent 21499 fbd6422a847a
child 21501 8dab1e45c11f
renamed Args.Name to Args.Text;
src/Pure/Isar/rule_insts.ML
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Thu Nov 23 20:33:39 2006 +0100
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Thu Nov 23 20:33:41 2006 +0100
     1.3 @@ -66,10 +66,10 @@
     1.4      val (type_insts, term_insts) = List.partition (is_tvar o fst) mixed_insts;
     1.5      val internal_insts = term_insts |> map_filter
     1.6        (fn (xi, Args.Term t) => SOME (xi, t)
     1.7 -        | (_, Args.Name _) => NONE
     1.8 +        | (_, Args.Text _) => NONE
     1.9          | (xi, _) => error_var "Term argument expected for " xi);
    1.10      val external_insts = term_insts |> map_filter
    1.11 -      (fn (xi, Args.Name s) => SOME (xi, s) | _ => NONE);
    1.12 +      (fn (xi, Args.Text s) => SOME (xi, s) | _ => NONE);
    1.13  
    1.14  
    1.15      (* mixed type instantiations *)
    1.16 @@ -79,7 +79,7 @@
    1.17          val S = the_sort tvars xi;
    1.18          val T =
    1.19            (case arg of
    1.20 -            Args.Name s => ProofContext.read_typ ctxt s
    1.21 +            Args.Text s => ProofContext.read_typ ctxt s
    1.22            | Args.Typ T => T
    1.23            | _ => error_var "Type argument expected for " xi);
    1.24        in
    1.25 @@ -169,7 +169,7 @@
    1.26  val value =
    1.27    Args.internal_typ >> Args.Typ ||
    1.28    Args.internal_term >> Args.Term ||
    1.29 -  Args.name >> Args.Name;
    1.30 +  Args.name >> Args.Text;
    1.31  
    1.32  val inst = Args.var -- (Args.$$$ "=" |-- Args.ahead -- value)
    1.33    >> (fn (xi, (a, v)) => (a, (xi, v)));
    1.34 @@ -188,7 +188,7 @@
    1.35  
    1.36  val value =
    1.37    Args.internal_term >> Args.Term ||
    1.38 -  Args.name >> Args.Name;
    1.39 +  Args.name >> Args.Text;
    1.40  
    1.41  val inst = Args.ahead -- Args.maybe value;
    1.42  val concl = Args.$$$ "concl" -- Args.colon;