1.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml	Wed Jun 03 09:56:24 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Wed Jun 03 11:25:19 2020 +0200
     1.3 @@ -59,7 +59,7 @@
     1.4    let
     1.5      val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
     1.6  		  (((TermC.inst_bdv bdv) o Eval.norm o #prop o Thm.rep_thm) thm) ct
     1.7 -  in if rew then SOME (t', distinct asms) else NONE end
     1.8 +  in if rew then SOME (t', distinct op = asms) else NONE end
     1.9    (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)
    1.10  and rew_sub thy i bdv tless rls put_asm lrd r t = 
    1.11    (let
    1.12 @@ -135,7 +135,7 @@
    1.13      let
    1.14        val _= trace i (" rls: " ^ Rule_Set.id rrls ^ " on: " ^ UnparseC.term_in_thy thy t)
    1.15  	    val (t', asm, rew) = app_rev thy (i + 1) rrls t                   
    1.16 -    in if rew then SOME (t', distinct asm) else NONE end
    1.17 +    in if rew then SOME (t', distinct op = asm) else NONE end
    1.18    | rewrite__set_ thy i put_asm bdv rls ct =          (* Rls, Seq containing Thms or Eval, Cal1 *)
    1.19      let
    1.20        (* attention with cp to test/..: unbound thy, i, bdv, rls; TODO1803? pull out to rewrite__*)
    1.21 @@ -192,7 +192,7 @@
    1.22        val ruls = (#rules o Rule_Set.rep) rls;
    1.23        val _ = trace i (" rls: " ^ Rule_Set.id rls ^ " on: " ^ UnparseC.term_in_thy thy ct)
    1.24        val (ct', asm') = rew_once ruls [] ct Noap ruls;
    1.25 -	  in if ct = ct' then NONE else SOME (ct', distinct asm') end
    1.26 +	  in if ct = ct' then NONE else SOME (ct', distinct op =  asm') end
    1.27  (*-------------------------------------------------------------*)
    1.28  and app_rev thy i rrls t =            (* apply an Rrls; if not applicable proceed with subterms *)
    1.29    let (* check a (precond, pattern) of a rev-set; stops with 1st true *)