src/Pure/Isar/rule_insts.ML
changeset 36959 f5417836dbea
parent 36950 75b8f26f2f07
child 37145 01aa36932739
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Mon May 17 15:05:32 2010 +0200
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Mon May 17 15:11:25 2010 +0200
     1.3 @@ -29,9 +29,6 @@
     1.4  structure RuleInsts: RULE_INSTS =
     1.5  struct
     1.6  
     1.7 -structure T = OuterLex;
     1.8 -
     1.9 -
    1.10  (** reading instantiations **)
    1.11  
    1.12  local
    1.13 @@ -100,11 +97,11 @@
    1.14  
    1.15      val (type_insts, term_insts) = List.partition (is_tvar o fst) mixed_insts;
    1.16      val internal_insts = term_insts |> map_filter
    1.17 -      (fn (xi, T.Term t) => SOME (xi, t)
    1.18 -        | (_, T.Text _) => NONE
    1.19 +      (fn (xi, Token.Term t) => SOME (xi, t)
    1.20 +        | (_, Token.Text _) => NONE
    1.21          | (xi, _) => error_var "Term argument expected for " xi);
    1.22      val external_insts = term_insts |> map_filter
    1.23 -      (fn (xi, T.Text s) => SOME (xi, s) | _ => NONE);
    1.24 +      (fn (xi, Token.Text s) => SOME (xi, s) | _ => NONE);
    1.25  
    1.26  
    1.27      (* mixed type instantiations *)
    1.28 @@ -114,8 +111,8 @@
    1.29          val S = the_sort tvars xi;
    1.30          val T =
    1.31            (case arg of
    1.32 -            T.Text s => Syntax.read_typ ctxt s
    1.33 -          | T.Typ T => T
    1.34 +            Token.Text s => Syntax.read_typ ctxt s
    1.35 +          | Token.Typ T => T
    1.36            | _ => error_var "Type argument expected for " xi);
    1.37        in
    1.38          if Sign.of_sort thy (T, S) then ((xi, S), T)
    1.39 @@ -172,9 +169,9 @@
    1.40      val _ = (*assign internalized values*)
    1.41        mixed_insts |> List.app (fn (arg, (xi, _)) =>
    1.42          if is_tvar xi then
    1.43 -          T.assign (SOME (T.Typ (the (AList.lookup (op =) type_insts xi)))) arg
    1.44 +          Token.assign (SOME (Token.Typ (the (AList.lookup (op =) type_insts xi)))) arg
    1.45          else
    1.46 -          T.assign (SOME (T.Term (the (AList.lookup (op =) term_insts xi)))) arg);
    1.47 +          Token.assign (SOME (Token.Term (the (AList.lookup (op =) term_insts xi)))) arg);
    1.48    in
    1.49      Drule.instantiate insts thm |> Rule_Cases.save thm
    1.50    end;
    1.51 @@ -197,7 +194,7 @@
    1.52  
    1.53  fun read_instantiate ctxt args thm =
    1.54    read_instantiate_mixed (ctxt |> ProofContext.set_mode ProofContext.mode_schematic)  (* FIXME !? *)
    1.55 -    (map (fn (x, y) => (T.eof, (x, T.Text y))) args) thm;
    1.56 +    (map (fn (x, y) => (Token.eof, (x, Token.Text y))) args) thm;
    1.57  
    1.58  fun instantiate_tac ctxt args = PRIMITIVE (read_instantiate ctxt args);
    1.59  
    1.60 @@ -210,9 +207,9 @@
    1.61  local
    1.62  
    1.63  val value =
    1.64 -  Args.internal_typ >> T.Typ ||
    1.65 -  Args.internal_term >> T.Term ||
    1.66 -  Args.name_source >> T.Text;
    1.67 +  Args.internal_typ >> Token.Typ ||
    1.68 +  Args.internal_term >> Token.Term ||
    1.69 +  Args.name_source >> Token.Text;
    1.70  
    1.71  val inst = Args.var -- (Args.$$$ "=" |-- Scan.ahead Parse.not_eof -- value)
    1.72    >> (fn (xi, (a, v)) => (a, (xi, v)));
    1.73 @@ -233,8 +230,8 @@
    1.74  local
    1.75  
    1.76  val value =
    1.77 -  Args.internal_term >> T.Term ||
    1.78 -  Args.name_source >> T.Text;
    1.79 +  Args.internal_term >> Token.Term ||
    1.80 +  Args.name_source >> Token.Text;
    1.81  
    1.82  val inst = Scan.ahead Parse.not_eof -- Args.maybe value;
    1.83  val concl = Args.$$$ "concl" -- Args.colon;