author blanchet Wed, 30 Jul 2014 23:52:56 +0200 changeset 57717 949838aba487 parent 57716 4546c9fdd8a7 child 57718 892e8e7a42b3
unlift before uncombine, because the definition of a lambda-lifted symbol might have an SK combinator in it (in hybrid encodings)
```--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Jul 30 14:03:58 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Jul 30 23:52:56 2014 +0200
@@ -569,25 +569,26 @@

fun uncombine_term thy =
let
-    fun aux (t1 \$ t2) = betapply (pairself aux (t1, t2))
-      | aux (Abs (s, T, t')) = Abs (s, T, aux t')
-      | aux (t as Const (x as (s, _))) =
+    fun uncomb (t1 \$ t2) = betapply (uncomb t1, uncomb t2)
+      | uncomb (Abs (s, T, t)) = Abs (s, T, uncomb t)
+      | uncomb (t as Const (x as (s, _))) =
(case AList.lookup (op =) combinator_table s of
SOME thm => thm |> prop_of |> specialize_type thy x |> Logic.dest_equals |> snd
| NONE => t)
-      | aux t = t
-  in aux end
+      | uncomb t = t
+  in uncomb end

-fun unlift_term lifted =
-  map_aterms (fn t as Const (s, _) =>
-                 if String.isPrefix lam_lifted_prefix s then
-                   (* FIXME: do something about the types *)
-                   (case AList.lookup (op =) lifted s of
-                     SOME t => unlift_term lifted t
-                   | NONE => t)
-                 else
-                   t
-               | t => t)
+fun unlift_aterm lifted (t as Const (s, _)) =
+    if String.isPrefix lam_lifted_prefix s then
+      (* FIXME: do something about the types *)
+      (case AList.lookup (op =) lifted s of
+        SOME t' => unlift_term lifted t'
+      | NONE => t)
+    else
+      t
+  | unlift_aterm _ t = t
+and unlift_term lifted =
+  map_aterms (unlift_aterm lifted)

fun termify_line _ _ _ _ _ (_, Type_Role, _, _, _) = NONE
| termify_line ctxt format type_enc lifted sym_tab (name, role, u, rule, deps) =
@@ -595,8 +596,8 @@
val thy = Proof_Context.theory_of ctxt
val t = u
|> prop_of_atp ctxt format type_enc true sym_tab
+        |> unlift_term lifted
|> uncombine_term thy
-        |> unlift_term lifted
in
SOME (name, role, t, rule, deps)
end```