src/HOL/Modelcheck/MCSyn.ML

 	((cut_facts_tac [OraAss] i) THEN (atac i)) state
         end
 end;
 
 
-goalw thy [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))";
+Goalw [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))";
   by (rtac ext 1);
   by (stac (surjective_pairing RS sym) 1);
   by (rtac refl 1);
 qed "pair_eta_expand";