IOA/meta_theory/Solve.ML

--- a/IOA/meta_theory/Solve.ML	Fri Nov 11 10:35:03 1994 +0100
+++ b/IOA/meta_theory/Solve.ML	Mon Nov 21 17:50:34 1994 +0100
@@ -50,4 +50,4 @@
   by (eres_inst_tac [("x","snd(ex,Suc(n))")] allE 1);
   by (eres_inst_tac [("x","a")] allE 1);
   by (asm_full_simp_tac SS 1);
-val trace_inclusion = result();
+qed "trace_inclusion";