Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/nominal_function_core.ML
changeset 2974 b95a2065aa10
parent 2973 d1038e67923a
child 2994 4ee772b12032 
--- a/Nominal/nominal_function_core.ML	Mon Jul 18 17:40:13 2011 +0100
+++ b/Nominal/nominal_function_core.ML	Tue Jul 19 01:40:36 2011 +0100
@@ -1053,16 +1053,15 @@
       let
         val newthy = theory_of_thm provedgoal (*FIXME*)
 
-        val (graph_is_function, complete_thm) =
+        val ((graph_is_function, complete_thm), graph_is_eqvt) =
           provedgoal
-          |> fst o Conjunction.elim
-          |> fst o Conjunction.elim
           |> Conjunction.elim
-          |> apfst (Thm.forall_elim_vars 0)
+          |>> fst o Conjunction.elim
+          |>> Conjunction.elim
+          |>> apfst (Thm.forall_elim_vars 0)
 
         val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)
-
-        val f_eqvt = graph_is_function RS (G_eqvt RS (f_defthm RS @{thm fundef_ex1_eqvt}))
+        val f_eqvt = graph_is_function RS (graph_is_eqvt RS (f_defthm RS @{thm fundef_ex1_eqvt}))
 
         val psimps = PROFILE "Proving simplification rules"
           (mk_psimps newthy globals R xclauses values f_iff) graph_is_function
nominal2