simplified sectioned_args;
authorwenzelm
Sat Sep 25 13:08:54 1999 +0200 (1999-09-25 ago)
changeset 7601c568799bf21b
parent 7600 73f91da46230
child 7602 2c0f407f80ce
simplified sectioned_args;
tuned;
src/Pure/Isar/method.ML
     1.1 --- a/src/Pure/Isar/method.ML	Sat Sep 25 13:08:08 1999 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Sat Sep 25 13:08:54 1999 +0200
     1.3 @@ -21,8 +21,8 @@
     1.4    val insert_tac: thm list -> int -> tactic
     1.5    val insert: thm list -> Proof.method
     1.6    val insert_facts: Proof.method
     1.7 +  val unfold: thm list -> Proof.method
     1.8    val fold: thm list -> Proof.method
     1.9 -  val unfold: thm list -> Proof.method
    1.10    val multi_resolve: thm list -> thm -> thm Seq.seq
    1.11    val multi_resolves: thm list -> thm list -> thm Seq.seq
    1.12    val rule_tac: thm list -> thm list -> int -> tactic
    1.13 @@ -40,13 +40,14 @@
    1.14    val ctxt_args: (Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
    1.15    val no_args: Proof.method -> Args.src -> Proof.context -> Proof.method
    1.16    type modifier
    1.17 -  val sectioned_args: ((Args.T list -> modifier * Args.T list) list ->
    1.18 -      Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
    1.19 +  val sectioned_args: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
    1.20      (Args.T list -> modifier * Args.T list) list ->
    1.21      ('a -> Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
    1.22 -  val bang_sectioned_args: (Args.T list -> modifier * Args.T list) list ->
    1.23 +  val bang_sectioned_args:
    1.24 +    (Args.T list -> modifier * Args.T list) list ->
    1.25      (thm list -> Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
    1.26 -  val only_sectioned_args: (Args.T list -> modifier * Args.T list) list ->
    1.27 +  val only_sectioned_args:
    1.28 +    (Args.T list -> modifier * Args.T list) list ->
    1.29      (Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
    1.30    val thms_args: (thm list -> Proof.method) -> Args.src -> Proof.context -> Proof.method
    1.31    datatype text =
    1.32 @@ -116,10 +117,10 @@
    1.33  end;
    1.34  
    1.35  
    1.36 -(* fold / unfold definitions *)
    1.37 +(* unfold / fold definitions *)
    1.38  
    1.39 +fun unfold thms = METHOD (fn facts => ALLGOALS (insert_tac facts) THEN rewrite_goals_tac thms);
    1.40  fun fold thms = METHOD (fn facts => ALLGOALS (insert_tac facts) THEN fold_goals_tac thms);
    1.41 -fun unfold thms = METHOD (fn facts => ALLGOALS (insert_tac facts) THEN rewrite_goals_tac thms);
    1.42  
    1.43  
    1.44  (* multi_resolve *)
    1.45 @@ -283,7 +284,7 @@
    1.46  fun section ss = (sect ss -- thmss ss) :-- (fn (m, ths) => Scan.depend (fn ctxt =>
    1.47    Scan.succeed (apply m (ctxt, ths)))) >> #2;
    1.48  
    1.49 -fun sectioned args ss = args ss -- Scan.repeat (section ss);
    1.50 +fun sectioned args ss = args -- Scan.repeat (section ss);
    1.51  
    1.52  in
    1.53  
    1.54 @@ -291,10 +292,10 @@
    1.55    let val (ctxt', (x, _)) = syntax (sectioned args ss) ctxt src
    1.56    in f x ctxt' end;
    1.57  
    1.58 -fun bang_sectioned_args ss f = sectioned_args (K Args.bang_facts) ss f;
    1.59 -fun only_sectioned_args ss f = sectioned_args (K (Scan.succeed ())) ss (fn () => f);
    1.60 +fun bang_sectioned_args ss f = sectioned_args Args.bang_facts ss f;
    1.61 +fun only_sectioned_args ss f = sectioned_args (Scan.succeed ()) ss (fn () => f);
    1.62  
    1.63 -fun thms_args f = sectioned_args thmss [] (fn ths => fn _ => f ths);
    1.64 +fun thms_args f = sectioned_args (thmss []) [] (fn ths => fn _ => f ths);
    1.65  
    1.66  end;
    1.67  
    1.68 @@ -382,8 +383,8 @@
    1.69    ("succeed", no_args succeed, "succeed"),
    1.70    ("-", no_args insert_facts, "do nothing, inserting current facts only"),
    1.71    ("insert", thms_args insert, "insert facts (improper!)"),
    1.72 -  ("fold", thms_args fold, "fold definitions, ignoring facts"),
    1.73 -  ("unfold", thms_args unfold, "unfold definitions, ignoring facts"),
    1.74 +  ("unfold", thms_args unfold, "unfold definitions"),
    1.75 +  ("fold", thms_args fold, "fold definitions"),
    1.76    ("rule", thms_args rule, "apply some rule"),
    1.77    ("erule", thms_args erule, "apply some erule (improper!)"),
    1.78    ("assumption", ctxt_args assumption, "proof by assumption, preferring facts")];