src/HOL/List.thy

   end;
 
 in
 
 val list_eq_simproc =
-  Simplifier.simproc @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq);
+  Simplifier.simproc (the_context ()) "list_eq" ["(xs::'a list) = ys"] (K list_eq);
 
 end;
 
 Addsimprocs [list_eq_simproc];
 *}