src/Pure/Isar/method.ML
changeset 8282 58a33fd5b30c
parent 8242 ac8ac0eba738
child 8329 8308b7a152a3
     1.1 --- a/src/Pure/Isar/method.ML	Tue Feb 22 21:50:02 2000 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Tue Feb 22 21:51:25 2000 +0100
     1.3 @@ -50,7 +50,7 @@
     1.4    val add_methods: (bstring * (Args.src -> Proof.context -> Proof.method) * string) list
     1.5      -> theory -> theory
     1.6    val syntax: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
     1.7 -    Proof.context -> Args.src -> Proof.context * 'a
     1.8 +    Args.src -> Proof.context -> Proof.context * 'a
     1.9    val ctxt_args: (Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
    1.10    val no_args: Proof.method -> Args.src -> Proof.context -> Proof.method
    1.11    type modifier
    1.12 @@ -403,7 +403,7 @@
    1.13    Args.syntax "method" scan;
    1.14  
    1.15  fun ctxt_args (f: Proof.context -> Proof.method) src ctxt =
    1.16 -  #2 (syntax (Scan.succeed (f ctxt)) ctxt src);
    1.17 +  #2 (syntax (Scan.succeed (f ctxt)) src ctxt);
    1.18  
    1.19  fun no_args m = ctxt_args (K m);
    1.20  
    1.21 @@ -428,7 +428,7 @@
    1.22  in
    1.23  
    1.24  fun sectioned_args args ss f src ctxt =
    1.25 -  let val (ctxt', (x, _)) = syntax (sectioned args ss) ctxt src
    1.26 +  let val (ctxt', (x, _)) = syntax (sectioned args ss) src ctxt
    1.27    in f x ctxt' end;
    1.28  
    1.29  fun bang_sectioned_args ss f = sectioned_args Args.bang_facts ss f;
    1.30 @@ -447,7 +447,7 @@
    1.31      Args.enum1 "and" (Scan.lift (Args.name -- Args.!!! (Args.$$$ "=" |-- Args.name))) --
    1.32      (Scan.lift (Args.$$$ "in") |-- Attrib.local_thm);
    1.33  
    1.34 -fun inst_args f src ctxt = f ((#2 oo syntax insts) ctxt src);
    1.35 +fun inst_args f = f oo (#2 oo syntax insts);
    1.36  
    1.37  
    1.38