src/Pure/Isar/method.ML
changeset 15703 727ef1b8b3ee
parent 15574 b1d1b5bfc464
child 15713 64a134029fe4
     1.1 --- a/src/Pure/Isar/method.ML	Wed Apr 13 09:48:41 2005 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Wed Apr 13 18:34:22 2005 +0200
     1.3 @@ -15,6 +15,7 @@
     1.4  signature METHOD =
     1.5  sig
     1.6    include BASIC_METHOD
     1.7 +  type src
     1.8    val trace: Proof.context -> thm list -> unit
     1.9    val RAW_METHOD: (thm list -> tactic) -> Proof.method
    1.10    val RAW_METHOD_CASES:
    1.11 @@ -48,37 +49,37 @@
    1.12    val set_tactic: (Proof.context -> thm list -> tactic) -> unit
    1.13    val tactic: string -> Proof.context -> Proof.method
    1.14    exception METHOD_FAIL of (string * Position.T) * exn
    1.15 -  val method: theory -> Args.src -> Proof.context -> Proof.method
    1.16 -  val add_method: bstring * (Args.src -> Proof.context -> Proof.method) * string
    1.17 +  val method: theory -> src -> Proof.context -> Proof.method
    1.18 +  val add_method: bstring * (src -> Proof.context -> Proof.method) * string
    1.19      -> theory -> theory
    1.20 -  val add_methods: (bstring * (Args.src -> Proof.context -> Proof.method) * string) list
    1.21 +  val add_methods: (bstring * (src -> Proof.context -> Proof.method) * string) list
    1.22      -> theory -> theory
    1.23    val syntax: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
    1.24 -    Args.src -> Proof.context -> Proof.context * 'a
    1.25 +    src -> Proof.context -> Proof.context * 'a
    1.26    val simple_args: (Args.T list -> 'a * Args.T list)
    1.27 -    -> ('a -> Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
    1.28 -  val ctxt_args: (Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
    1.29 -  val no_args: Proof.method -> Args.src -> Proof.context -> Proof.method
    1.30 +    -> ('a -> Proof.context -> Proof.method) -> src -> Proof.context -> Proof.method
    1.31 +  val ctxt_args: (Proof.context -> Proof.method) -> src -> Proof.context -> Proof.method
    1.32 +  val no_args: Proof.method -> src -> Proof.context -> Proof.method
    1.33    type modifier
    1.34    val sectioned_args: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
    1.35      (Args.T list -> modifier * Args.T list) list ->
    1.36 -    ('a -> Proof.context -> 'b) -> Args.src -> Proof.context -> 'b
    1.37 +    ('a -> Proof.context -> 'b) -> src -> Proof.context -> 'b
    1.38    val bang_sectioned_args:
    1.39      (Args.T list -> modifier * Args.T list) list ->
    1.40 -    (thm list -> Proof.context -> 'a) -> Args.src -> Proof.context -> 'a
    1.41 +    (thm list -> Proof.context -> 'a) -> src -> Proof.context -> 'a
    1.42    val bang_sectioned_args':
    1.43      (Args.T list -> modifier * Args.T list) list ->
    1.44      (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
    1.45 -    ('a -> thm list -> Proof.context -> 'b) -> Args.src -> Proof.context -> 'b
    1.46 +    ('a -> thm list -> Proof.context -> 'b) -> src -> Proof.context -> 'b
    1.47    val only_sectioned_args:
    1.48      (Args.T list -> modifier * Args.T list) list ->
    1.49 -    (Proof.context -> 'a) -> Args.src -> Proof.context -> 'a
    1.50 -  val thms_ctxt_args: (thm list -> Proof.context -> 'a) -> Args.src -> Proof.context -> 'a
    1.51 -  val thms_args: (thm list -> 'a) -> Args.src -> Proof.context -> 'a
    1.52 -  val thm_args: (thm -> 'a) -> Args.src -> Proof.context -> 'a
    1.53 +    (Proof.context -> 'a) -> src -> Proof.context -> 'a
    1.54 +  val thms_ctxt_args: (thm list -> Proof.context -> 'a) -> src -> Proof.context -> 'a
    1.55 +  val thms_args: (thm list -> 'a) -> src -> Proof.context -> 'a
    1.56 +  val thm_args: (thm -> 'a) -> src -> Proof.context -> 'a
    1.57    datatype text =
    1.58      Basic of (Proof.context -> Proof.method) |
    1.59 -    Source of Args.src |
    1.60 +    Source of src |
    1.61      Then of text list |
    1.62      Orelse of text list |
    1.63      Try of text |
    1.64 @@ -107,19 +108,21 @@
    1.65      theory * ((string * string) * (string * thm list) list)
    1.66    val global_done_proof: Proof.state -> theory * ((string * string) * (string * thm list) list)
    1.67    val goal_args: (Args.T list -> 'a * Args.T list) -> ('a -> int -> tactic)
    1.68 -    -> Args.src -> Proof.context -> Proof.method
    1.69 +    -> src -> Proof.context -> Proof.method
    1.70    val goal_args': (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))
    1.71 -    -> ('a -> int -> tactic) -> Args.src -> Proof.context -> Proof.method
    1.72 +    -> ('a -> int -> tactic) -> src -> Proof.context -> Proof.method
    1.73    val goal_args_ctxt: (Args.T list -> 'a * Args.T list) -> (Proof.context -> 'a -> int -> tactic)
    1.74 -    -> Args.src -> Proof.context -> Proof.method
    1.75 +    -> src -> Proof.context -> Proof.method
    1.76    val goal_args_ctxt': (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))
    1.77 -    -> (Proof.context -> 'a -> int -> tactic) -> Args.src -> Proof.context -> Proof.method
    1.78 +    -> (Proof.context -> 'a -> int -> tactic) -> src -> Proof.context -> Proof.method
    1.79    val setup: (theory -> theory) list
    1.80  end;
    1.81  
    1.82  structure Method: METHOD =
    1.83  struct
    1.84  
    1.85 +type src = Args.src;
    1.86 +
    1.87  
    1.88  (** proof methods **)
    1.89  
    1.90 @@ -374,7 +377,7 @@
    1.91                | some => some)
    1.92            | types' xi = types xi;
    1.93          fun internal x = isSome (types' (x, ~1));
    1.94 -        val used = Term.add_term_tvarnames (Thm.prop_of st $ Thm.prop_of thm, []);
    1.95 +        val used = Drule.add_used thm (Drule.add_used st []);
    1.96          val (ts, envT) =
    1.97            ProofContext.read_termTs_schematic ctxt internal types' sorts used (ss ~~ Ts);
    1.98          val cenvT = map (apsnd (Thm.ctyp_of sign)) (envT @ Tinsts_env);
    1.99 @@ -505,7 +508,7 @@
   1.100    val name = "Isar/methods";
   1.101    type T =
   1.102      {space: NameSpace.T,
   1.103 -     meths: (((Args.src -> Proof.context -> Proof.method) * string) * stamp) Symtab.table};
   1.104 +     meths: (((src -> Proof.context -> Proof.method) * string) * stamp) Symtab.table};
   1.105  
   1.106    val empty = {space = NameSpace.empty, meths = Symtab.empty};
   1.107    val copy = I;
   1.108 @@ -692,7 +695,7 @@
   1.109  
   1.110  datatype text =
   1.111    Basic of (Proof.context -> Proof.method) |
   1.112 -  Source of Args.src |
   1.113 +  Source of src |
   1.114    Then of text list |
   1.115    Orelse of text list |
   1.116    Try of text |