src/Sequents/prover.ML
changeset 38500 d5477ee35820
parent 33049 c38f02fdf35d
child 55228 901a6696cdd8
--- a/src/Sequents/prover.ML	Tue Aug 17 19:36:38 2010 +0200
+++ b/src/Sequents/prover.ML	Tue Aug 17 19:36:39 2010 +0200
@@ -55,7 +55,7 @@
     ["Unsafe rules:"] @ map Display.string_of_thm_without_context unsafes));
 
 (*Returns the list of all formulas in the sequent*)
-fun forms_of_seq (Const("SeqO'",_) $ P $ u) = P :: forms_of_seq u
+fun forms_of_seq (Const(@{const_name "SeqO'"},_) $ P $ u) = P :: forms_of_seq u
   | forms_of_seq (H $ u) = forms_of_seq u
   | forms_of_seq _ = [];