1.1 --- a/src/Tools/isac/Knowledge/Simplify.thy	Wed Sep 29 19:34:32 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy	Tue Nov 16 18:26:57 2021 +0100
     1.3 @@ -48,9 +48,9 @@
     1.4  				  "Simplify (2*a + 3*a)");
     1.5     *)
     1.6  fun argl2dtss t =
     1.7 -    [((Thm.term_of o the o (TermC.parse @{theory})) "Term", t),
     1.8 -     ((Thm.term_of o the o (TermC.parse @{theory})) "normalform", 
     1.9 -      [(Thm.term_of o the o (TermC.parse @{theory})) "N"])
    1.10 +    [((TermC.parseNEW''\<^theory>) "Term", t),
    1.11 +     ((TermC.parseNEW''\<^theory>) "normalform", 
    1.12 +     [(TermC.parseNEW''\<^theory>) "N"])
    1.13       ]
    1.14    (*| argl2dtss _ = raise ERROR "Simplify.ML: wrong argument for argl2dtss"*);
    1.15  \<close>