1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Sun Sep 12 15:53:36 2021 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Sun Sep 12 16:18:03 2021 +0200
     1.3 @@ -439,7 +439,7 @@
     1.4  (*("argument_in" ,("Prog_Expr.argument_in", Prog_Expr.eval_argument_in "Prog_Expr.argument_in"))*)
     1.5  fun eval_argument_in _ "Prog_Expr.argument_in" 
     1.6  		 (t as (Const ("Prog_Expr.argument_in", _) $ (_(*f*) $ arg))) _ =
     1.7 -    if is_Free arg (*could be something to be simplified before*)
     1.8 +    if TermC.is_atom arg (*could be something to be simplified before*)
     1.9      then
    1.10        SOME (UnparseC.term t ^ " = " ^ UnparseC.term arg,
    1.11  	      HOLogic.Trueprop $ (TermC.mk_equality (t, arg)))

     2.1 --- a/test/Tools/isac/Knowledge/biegelinie-1.sml	Sun Sep 12 15:53:36 2021 +0200
     2.2 +++ b/test/Tools/isac/Knowledge/biegelinie-1.sml	Sun Sep 12 16:18:03 2021 +0200
     2.3 @@ -62,9 +62,9 @@
     2.4  				   Eval("Groups.plus_class.plus", eval_binop "#add_")
     2.5  				   ], 
     2.6  		srls = Rule_Set.Empty, calc = [], errpatts = [],
     2.7 -		rules = [Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
     2.8 +		rules = [Thm ("NTH_CONS", @{thm NTH_CONS}),
     2.9  			 Eval("Groups.plus_class.plus", eval_binop "#add_"),
    2.10 -			 Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
    2.11 +			 Thm ("NTH_NIL", @{thm NTH_NIL}),
    2.12  			 Eval("Prog_Expr.lhs", eval_lhs "eval_lhs_"),
    2.13  			 Eval("Prog_Expr.rhs", eval_rhs "eval_rhs_"),
    2.14  			 Eval("Prog_Expr.argument_in", eval_argument_in "Prog_Expr.argument_in")
    2.15 @@ -76,9 +76,7 @@
    2.16    (TermC.str2term "(NTH::[real,bool list]=>bool) 1 " $ rm_);
    2.17  if UnparseC.term e1__ = "M_b 0 = 0" then () else error "biegelinie.sml simplify NTH 1 rm_";
    2.18  
    2.19 -val SOME (x1__,_) = 
    2.20 -    rewrite_set_ thy false srls 
    2.21 -		 (TermC.str2term"argument_in (lhs (M_b 0 = 0))");
    2.22 +val SOME (x1__,_) = rewrite_set_ thy false srls (TermC.str2term "argument_in (lhs (M_b 0 = 0))");
    2.23  if UnparseC.term x1__ = "0" then ()
    2.24  else error "biegelinie.sml simplify argument_in (lhs (M_b 0 = 0)";
    2.25  

     3.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Sun Sep 12 15:53:36 2021 +0200
     3.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Sun Sep 12 16:18:03 2021 +0200
     3.3 @@ -307,7 +307,7 @@
     3.4    ML_file "Knowledge/polyminus.sml"
     3.5    ML_file "Knowledge/vect.sml"
     3.6    ML_file "Knowledge/diffapp.sml"        (* postponed to dev. specification | TP-prog. *)
     3.7 -(*ML_file "Knowledge/biegelinie-1.sml"          (**) TOODOO.1 requires integrate.sml, eqsystem.sml*)
     3.8 +  ML_file "Knowledge/biegelinie-1.sml"
     3.9  (*ML_file "Knowledge/biegelinie-2.sml"                                          Test_Isac_Short*)
    3.10  (*ML_file "Knowledge/biegelinie-3.sml"                                          Test_Isac_Short*)
    3.11  (*ML_file "Knowledge/biegelinie-4.sml"          (**) TOODOO.1 requires integrate.sml, eqsystem.sml*)