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