test/Tools/isac/Knowledge/algein.sml
changeset 59912 dc53f7815edc
parent 59911 ff30cec13f4f
child 59936 554030065b5b
     1.1 --- a/test/Tools/isac/Knowledge/algein.sml	Mon Apr 27 12:36:21 2020 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/algein.sml	Mon Apr 27 16:37:56 2020 +0200
     1.3 @@ -110,9 +110,9 @@
     1.4  
     1.5  (*testing code in ME/appl.sml*)
     1.6  val sube = ["?a1 = (3::real)"];
     1.7 -val subte = Subst.tyty_to_eqs sube;
     1.8 +val subte = Subst.input_to_terms sube;
     1.9  UnparseC.terms_short subte = "[?a1 = 3]"; (* = true*)
    1.10 -val subst = Subst.T_from_tyty thy sube;
    1.11 +val subst = Subst.T_from_string_eqs thy sube;
    1.12  foldl and_ (true, map contains_Var subte);
    1.13  
    1.14  val t'' = subst_atomic subst t';