1.1 --- a/src/Tools/isac/ProgLang/Prog_Tac.thy	Wed Oct 02 15:14:51 2019 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy	Wed Oct 02 16:02:17 2019 +0200
     1.3 @@ -37,11 +37,11 @@
     1.4    Calculate    :: "[char list, 'a] => 'a"
     1.5    Rewrite      :: "[char list, 'a] => 'a"
     1.6    Rewrite'_Inst:: "[(char list * 'b) list, char list, 'a] => 'a"
     1.7 -			               ("(Rewrite'_Inst (_ _))" 11) (*without last argument ^^ for @@*)
     1.8 +			               ("(Rewrite'_Inst (_ _))" 11) (*without last argument ^^ for #>*)
     1.9    Rewrite'_Set :: "[char list, 'a] => 'a" ("(Rewrite'_Set (_))" 11)
    1.10    Rewrite'_Set'_Inst
    1.11                 :: "[((char list) * 'b) list, char list, 'a] => 'a"
    1.12 -		                 ("(Rewrite'_Set'_Inst (_ _))" 11) (*without last argument ^^ for @@*)
    1.13 +		                 ("(Rewrite'_Set'_Inst (_ _))" 11) (*without last argument ^^ for #>*)
    1.14    Or'_to'_List :: "bool => 'a list"  ("Or'_to'_List (_)" 11)
    1.15    SubProblem   :: "[char list * char list list * char list list, arg list] => 'a"
    1.16    Substitute   :: "[bool list, 'a] => 'a"
    1.17 @@ -82,7 +82,7 @@
    1.18  (* get argument of first Prog_Tac in a progam for init_form *)
    1.19  fun get_stac thy (_ $ body) =
    1.20    let
    1.21 -    (* entries occur twice, for form curried by @@ or non-curried *)
    1.22 +    (* entries occur twice, for form curried by #> or non-curried *)
    1.23      fun get_t y (Const ("Tactical.Seq",_) $ e1 $ e2) a = 
    1.24      	  (case get_t y e1 a of NONE => get_t y e2 a | la => la)
    1.25        | get_t y (Const ("Tactical.Seq",_) $ e1 $ e2 $ a) _ = 
    1.26 @@ -124,7 +124,7 @@
    1.27  
    1.28  (* substitute the Istate.T's environment to a leaf of the program
    1.29     and attach the curried argument of a tactic, if any.
    1.30 -CAUTION: (1) currying with @@ requires 2 patterns for each tactic
    1.31 +CAUTION: (1) currying with #> requires 2 patterns for each tactic
    1.32           (2) the non-curried version must return NONE for a 
    1.33  	       (3) non-matching patterns become an Celem.Expr by fall-through.
    1.34  WN060906 quick and dirty fix: due to (2) a is returned, too *)