1.1 --- a/src/Tools/isac/BaseDefinitions/environment.sml	Wed Apr 28 12:38:13 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/environment.sml	Thu Apr 29 09:55:06 2021 +0200
     1.3 @@ -46,7 +46,7 @@
     1.4    curried Rewrite) for CURRENT value (which may be different from PREVIOUS);
     1.5    thus "NONE" must be set at the end of currying (ill designed anyway)*)
     1.6  fun update_opt env (SOME id, vl) = update env (id, vl)
     1.7 -  | update_opt env (NONE, vl) =
     1.8 +  | update_opt env (NONE, _) =
     1.9      ((** )tracing ("*** update_opt: (NONE," ^ UnparseC.term vl ^ ")");( **) env);
    1.10  fun update_opt' (env, (id, vl)) = update_opt env (id, vl)
    1.11  fun update_opt'' ((vl, env), id) = update_opt env (id, vl)

     2.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Wed Apr 28 12:38:13 2021 +0200
     2.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Thu Apr 29 09:55:06 2021 +0200
     2.3 @@ -530,8 +530,6 @@
     2.4    |> typ_a2real;       (*TODO drop*)
     2.5  fun str2term str = parse_patt (ThyC.get_theory "Isac_Knowledge") str
     2.6  
     2.7 -(* TODO decide with Test_Isac *)
     2.8 -fun is_atom t = length (vars t) = 1
     2.9  fun is_atom (Const ("Float.Float",_) $ _) = true
    2.10    | is_atom (Const ("ComplexI.I'_'_",_)) = true
    2.11    | is_atom (Const ("Groups.times_class.times",_) $ t $ Const ("ComplexI.I'_'_",_)) = is_atom t
    2.12 @@ -597,7 +595,8 @@
    2.13  fun raise_type_conflicts ts =
    2.14    let
    2.15      val dups = duplicates (op =) (map (fst o dest_Free) ts)
    2.16 -    val confl = filter (fn Free (str, _) => member op = dups str) ts
    2.17 +    val confl = filter (fn Free (str, _) => member op = dups str
    2.18 +                         | _ => false) ts
    2.19    in
    2.20      if confl = []
    2.21      then ()

     3.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml	Wed Apr 28 12:38:13 2021 +0200
     3.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml	Thu Apr 29 09:55:06 2021 +0200
     3.3 @@ -84,7 +84,8 @@
     3.4        \<close> of
     3.5        SOME xml => xml
     3.6      | NONE => sysERROR2xml 0 "error in kernel 2")
     3.7 -	| CalcTree [] = error "CalcTree: called with []"
     3.8 +	| CalcTree [] = raise ERROR "CalcTree: called with []"
     3.9 +	| CalcTree _ = raise ERROR "CalcTree: undef.case in fun.def"
    3.10  
    3.11  fun DEconstrCalcTree cI = deconstructcalctreeOK2xml (del_calc cI);
    3.12  fun getActiveFormula cI = iteratorOK2xml cI (get_pos cI 1);
    3.13 @@ -148,7 +149,8 @@
    3.14      	  in fetchproposedtacticOK2xml cI tac (Error_Pattern.from_store tac) end
    3.15    	| ("helpless", _) => fetchproposedtacticERROR2xml cI "helpless"
    3.16    	| ("no-fmz-spec", _) => fetchproposedtacticERROR2xml cI "no-fmz-spec"
    3.17 -  	| ("end-of-calculation", _) => fetchproposedtacticERROR2xml cI "end-of-calculation")
    3.18 +  	| ("end-of-calculation", _) => fetchproposedtacticERROR2xml cI "end-of-calculation"
    3.19 +    | _ => raise ERROR "fetchProposedTactic: undef.case")
    3.20      \<close> of
    3.21      SOME xml => xml
    3.22    | NONE => sysERROR2xml cI "error in kernel 3";
    3.23 @@ -403,7 +405,7 @@
    3.24      val pos = get_pos cI 1
    3.25    in
    3.26      case Step.do_next pos cs of
    3.27 -	    ("ok", cs' as (_, _, ptp)) =>
    3.28 +	    ("ok", (_, _, ptp)) =>
    3.29  	      (case Step_Solve.by_term ptp (encode ifo) of
    3.30  	        ("ok", (_(*use in DG !!!*), c, ptp as (_, p))) =>
    3.31  	          (upd_calc cI (ptp, []); upd_ipos cI 1 p;

     4.1 --- a/src/Tools/isac/Knowledge/Test_Build_Thydata.thy	Wed Apr 28 12:38:13 2021 +0200
     4.2 +++ b/src/Tools/isac/Knowledge/Test_Build_Thydata.thy	Thu Apr 29 09:55:06 2021 +0200
     4.3 @@ -46,7 +46,7 @@
     4.4    ("rls111",
     4.5      ("Test_Build_Thydata",
     4.6       Rule_Def.Repeat {calc = [], erls =
     4.7 -          Rule_Def.Repeat {calc = [], erls = Erls, errpatts = [], id = "empty", preconds = [], rew_ord =
     4.8 +          Rule_Def.Repeat {calc = [], erls = Rule_Set.Empty, errpatts = [], id = "empty", preconds = [], rew_ord =
     4.9                 ("dummy_ord", _), rules = [], scr = Empty_Prog, srls = Rule_Set.Empty},
    4.10            errpatts = [], id = "rls111", preconds = [], rew_ord = ("termlessI", _), rules =
    4.11            [Thm ("thm111", _), Thm ("refl", _)], scr = Empty_Prog, srls = Rule_Set.Empty})) => ()
    4.12 @@ -56,7 +56,7 @@
    4.13    ("rls222",
    4.14      ("Test_Build_Thydata",
    4.15       Rule_Def.Repeat {calc = [], erls =
    4.16 -          Rule_Def.Repeat {calc = [], erls = Erls, errpatts = [], id = "empty", preconds = [], rew_ord =
    4.17 +          Rule_Def.Repeat {calc = [], erls = Rule_Set.Empty, errpatts = [], id = "empty", preconds = [], rew_ord =
    4.18                 ("dummy_ord", _), rules = [], scr = Empty_Prog, srls = Rule_Set.Empty},
    4.19            errpatts = [], id = "rls222", preconds = [], rew_ord = ("termlessI", _), rules =
    4.20            [Thm ("sym_thm111", _), Thm ("o_def", _)], scr = Empty_Prog, srls = Rule_Set.Empty})) => ()