1.1 --- a/src/Tools/isac/Interpret/specification-elems.sml	Sun Feb 25 16:31:17 2018 +0100
     1.2 +++ b/src/Tools/isac/Interpret/specification-elems.sml	Fri Mar 02 14:19:59 2018 +0100
     1.3 @@ -122,9 +122,9 @@
     1.4  val subst2subs = map (pair2str o (apfst term2str) o (apsnd term2str));
     1.5  fun subst2sube subst = map term2str (map HOLogic.mk_eq subst)
     1.6  val subst2subs' = map ((apfst term2str) o (apsnd term2str));
     1.7 -fun subs2subst thy s = map (isapair2pair o (parse_patt thy)) s;
     1.8 -fun sube2subst thy s = map (dest_equals' o (parse_patt thy)) s;
     1.9 -val sube2subte = map str2term;
    1.10 +fun subs2subst thy s = map (TermC.isapair2pair o (TermC.parse_patt thy)) s;
    1.11 +fun sube2subst thy s = map (TermC.dest_equals' o (TermC.parse_patt thy)) s;
    1.12 +val sube2subte = map TermC.str2term;
    1.13  val subte2subst = map HOLogic.dest_eq;
    1.14  val e_ctxt = Proof_Context.init_global @{theory "Pure"};
    1.15