1.1 --- a/test/Tools/isac/Knowledge/algein.sml	Sun Oct 09 09:01:29 2022 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/algein.sml	Wed Oct 19 10:43:04 2022 +0200
     1.3 @@ -107,7 +107,9 @@
     1.4  UnparseC.term t' = "0 = ?a1 * 0"; (* = true*)
     1.5  
     1.6  val sube = ["?a1 = (3::real)"];
     1.7 -val subte = Subst.input_to_terms sube;
     1.8 +(*----------------vvvvvvvvvvvvvv ERROR Unbound schematic variable: ?a1
     1.9 +  --------------- review together with development of Widerspruch 3 = 77* )
    1.10 +val subte = Subst.input_to_terms @{context} sube;
    1.11  UnparseC.terms_short subte = "[?a1 = 3]"; (* = true*)
    1.12  val subst = Subst.T_from_string_eqs thy sube;
    1.13  foldl and_ (true, map TermC.contains_Var subte);
    1.14 @@ -119,4 +121,4 @@
    1.15  (*----- STOPPED.WN0x?: Widerspruch 3 = 777: sym contains "==>" instead of "=" !!!
    1.16  val SOME (t''',_) = rewrite_ thy rew_ord erls false thm t'';
    1.17  *)
    1.18 -
    1.19 +( *----------------^^^^^^^^^^^^^^ ERROR Unbound schematic variable: ?a1*)