src/Pure/Isar/rule_insts.ML
changeset 27809 a1e409db516b
parent 27378 0968c0d0b969
child 27882 eaa9fef9f4c1
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Sat Aug 09 12:28:13 2008 +0200
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Sat Aug 09 22:43:46 2008 +0200
     1.3 @@ -28,6 +28,9 @@
     1.4  structure RuleInsts: RULE_INSTS =
     1.5  struct
     1.6  
     1.7 +structure T = OuterLex;
     1.8 +structure P = OuterParse;
     1.9 +
    1.10  
    1.11  (** reading instantiations **)
    1.12  
    1.13 @@ -97,11 +100,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, Args.Term t) => SOME (xi, t)
    1.18 -        | (_, Args.Text _) => NONE
    1.19 +      (fn (xi, T.Term t) => SOME (xi, t)
    1.20 +        | (_, T.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, Args.Text s) => SOME (xi, s) | _ => NONE);
    1.24 +      (fn (xi, T.Text s) => SOME (xi, s) | _ => NONE);
    1.25  
    1.26  
    1.27      (* mixed type instantiations *)
    1.28 @@ -111,8 +114,8 @@
    1.29          val S = the_sort tvars xi;
    1.30          val T =
    1.31            (case arg of
    1.32 -            Args.Text s => Syntax.read_typ ctxt s
    1.33 -          | Args.Typ T => T
    1.34 +            T.Text s => Syntax.read_typ ctxt s
    1.35 +          | T.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 @@ -169,9 +172,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 -          Args.assign (SOME (Args.Typ (the (AList.lookup (op =) type_insts xi)))) arg
    1.44 +          T.assign (SOME (T.Typ (the (AList.lookup (op =) type_insts xi)))) arg
    1.45          else
    1.46 -          Args.assign (SOME (Args.Term (the (AList.lookup (op =) term_insts xi)))) arg);
    1.47 +          T.assign (SOME (T.Term (the (AList.lookup (op =) term_insts xi)))) arg);
    1.48    in
    1.49      Drule.instantiate insts thm |> RuleCases.save thm
    1.50    end;
    1.51 @@ -194,7 +197,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) => (Args.eof, (x, Args.Text y))) args) thm;
    1.56 +    (map (fn (x, y) => (T.eof, (x, T.Text y))) args) thm;
    1.57  
    1.58  fun instantiate_tac ctxt args = PRIMITIVE (read_instantiate ctxt args);
    1.59  
    1.60 @@ -207,16 +210,16 @@
    1.61  local
    1.62  
    1.63  val value =
    1.64 -  Args.internal_typ >> Args.Typ ||
    1.65 -  Args.internal_term >> Args.Term ||
    1.66 -  Args.name >> Args.Text;
    1.67 +  Args.internal_typ >> T.Typ ||
    1.68 +  Args.internal_term >> T.Term ||
    1.69 +  Args.name >> T.Text;
    1.70  
    1.71 -val inst = Args.var -- (Args.$$$ "=" |-- Args.ahead -- value)
    1.72 +val inst = Args.var -- (Args.$$$ "=" |-- Scan.ahead P.not_eof -- value)
    1.73    >> (fn (xi, (a, v)) => (a, (xi, v)));
    1.74  
    1.75  in
    1.76  
    1.77 -val where_att = Attrib.syntax (Args.and_list (Scan.lift inst) >> (fn args =>
    1.78 +val where_att = Attrib.syntax (Scan.lift (P.and_list inst) >> (fn args =>
    1.79    Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)));
    1.80  
    1.81  end;
    1.82 @@ -227,10 +230,10 @@
    1.83  local
    1.84  
    1.85  val value =
    1.86 -  Args.internal_term >> Args.Term ||
    1.87 -  Args.name >> Args.Text;
    1.88 +  Args.internal_term >> T.Term ||
    1.89 +  Args.name >> T.Text;
    1.90  
    1.91 -val inst = Args.ahead -- Args.maybe value;
    1.92 +val inst = Scan.ahead P.not_eof -- Args.maybe value;
    1.93  val concl = Args.$$$ "concl" -- Args.colon;
    1.94  
    1.95  val insts =
    1.96 @@ -406,16 +409,16 @@
    1.97  
    1.98  val insts =
    1.99    Scan.optional
   1.100 -    (Args.and_list1 (Scan.lift (Args.name -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
   1.101 -      Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
   1.102 +    (Scan.lift (P.and_list1 (Args.name -- (Args.$$$ "=" |-- P.!!! Args.name)) --| Args.$$$ "in")) []
   1.103 +    -- Attrib.thms;
   1.104  
   1.105  fun inst_args f src ctxt =
   1.106    f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts) src ctxt));
   1.107  
   1.108  val insts_var =
   1.109    Scan.optional
   1.110 -    (Args.and_list1 (Scan.lift (Args.var -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
   1.111 -      Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
   1.112 +    (Scan.lift (P.and_list1 (Args.var -- (Args.$$$ "=" |-- P.!!! Args.name)) --| Args.$$$ "in")) []
   1.113 +    -- Attrib.thms;
   1.114  
   1.115  fun inst_args_var f src ctxt =
   1.116    f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt));