# HG changeset patch
# User steckerm
# Date 1411202528 -7200
# Node ID ede6ca6a54eefe5699d3c254028aaf99973e4ca0
# Parent  623645fdb0472ffbcd6021cf543ee87cc4710f52
Added support for partial function application

diff -r 623645fdb047 -r ede6ca6a54ee src/HOL/Tools/ATP/atp_waldmeister.ML
--- a/src/HOL/Tools/ATP/atp_waldmeister.ML	Sat Sep 20 10:42:08 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_waldmeister.ML	Sat Sep 20 10:42:08 2014 +0200
@@ -6,8 +6,6 @@
 *)
 
 exception FailureMessage of string
-exception FailureTerm of term * term
-exception FailureWM of (term * term list * (string * string) list)
 
 signature ATP_WALDMEISTER_SKOLEMIZER =
 sig
@@ -49,95 +47,96 @@
 
 open HOLogic
 
-fun contains_quantor (Const (@{const_name Ex},_) $ _) = true
-  | contains_quantor (Const (@{const_name All},_) $ _) = true
+fun contains_quantor (Const (@{const_name Ex}, _) $ _) = true
+  | contains_quantor (Const (@{const_name All}, _) $ _) = true
   | contains_quantor (t1 $ t2) = contains_quantor t1 orelse contains_quantor t2
   | contains_quantor _ = false
 
-fun mk_fun_for_bvar ctxt1 ctxt2 arg_trms (bound_name,ty) =
+fun mk_fun_for_bvar ctxt1 ctxt2 arg_trms (bound_name, ty) =
   let
     val fun_type = (map type_of arg_trms) ---> ty
-    val (fun_name,_) = singleton (Variable.variant_frees ctxt2 []) ("sko_" ^ bound_name,fun_type)
-    val (_,ctxt1_new) = Variable.add_fixes [fun_name] ctxt1
-    val (_,ctxt2_new) = Variable.add_fixes [fun_name] ctxt2
+    val (fun_name, _) = singleton (Variable.variant_frees ctxt2 []) ("sko_" ^ bound_name,fun_type)
+    val (_, ctxt1_new) = Variable.add_fixes [fun_name] ctxt1
+    val (_, ctxt2_new) = Variable.add_fixes [fun_name] ctxt2
   in
-    (Term.list_comb (Free (fun_name,fun_type),arg_trms),ctxt1_new,ctxt2_new)
+    (Term.list_comb (Free (fun_name,fun_type), arg_trms), ctxt1_new, ctxt2_new)
+  end
+
+fun skolem_free ctxt1 ctxt2 vars (bound_name, ty, trm) =
+  let
+    val (fun_trm, ctxt1_new, ctxt2_new) = 
+      mk_fun_for_bvar ctxt1 ctxt2 (List.rev vars) (bound_name,ty)
+  in
+    (Term.subst_bounds ([fun_trm], trm), ctxt1_new, ctxt2_new)
   end
 
-fun skolem_free ctxt1 ctxt2 vars (bound_name,ty,trm) =
-    let
-      val (fun_trm,ctxt1_new,ctxt2_new) = mk_fun_for_bvar ctxt1 ctxt2 (List.rev vars) (bound_name,ty)
-    in
-      (Term.subst_bounds ([fun_trm],trm),ctxt1_new,ctxt2_new)
-    end
+fun skolem_var ctxt (bound_name, ty, trm) =
+  let
+    val (var_name, _) = singleton (Variable.variant_frees ctxt []) (bound_name, ty)
+    val (_, ctxt') = Variable.add_fixes [var_name] ctxt
+    val var = Var ((var_name, 0), ty)
+  in
+   (Term.subst_bounds ([var], trm), ctxt', var)
+  end
 
-fun skolem_var ctxt (bound_name,ty,trm) =
+fun skolem_bound is_free ctxt1 ctxt2 spets vars x =
+  if is_free then
+    let 
+      val (trm', ctxt1', ctxt2') = skolem_free ctxt1 ctxt2 vars x
+    in
+      (ctxt1', ctxt2',spets, trm', vars)
+    end
+  else
     let
-      val (var_name,_) = singleton (Variable.variant_frees ctxt []) (bound_name,ty)
-      val (_,ctxt') = Variable.add_fixes [var_name] ctxt
-      val var = Var ((var_name,0),ty)
+      val (trm', ctxt2', var) = skolem_var ctxt2 x
     in
-     (Term.subst_bounds ([var],trm),ctxt',var)
+      (ctxt1, ctxt2', spets, trm', var :: vars)
     end
 
-fun skolem_bound is_free ctxt1 ctxt2 spets vars x =
-    if is_free then
-      let 
-        val (trm',ctxt1',ctxt2') = skolem_free ctxt1 ctxt2 vars x
-      in
-        (ctxt1',ctxt2',spets,trm',vars)
-      end
+fun skolemize' pos ctxt1 ctxt2 spets vars (Const (@{const_name Not}, _) $ trm') =
+    let
+      val (ctxt1', ctxt2', spets', trm'') = skolemize' (not pos) ctxt1 ctxt2 spets vars trm'
+    in
+      (ctxt1', ctxt2', map mk_not spets', mk_not trm'')
+    end
+  | skolemize' pos ctxt1 ctxt2 spets vars (trm as (Const (@{const_name HOL.eq}, t) $ a $ b)) =
+    if t = @{typ "bool \<Rightarrow> bool \<Rightarrow> bool"} andalso contains_quantor trm then
+      skolemize' pos ctxt1 ctxt2 (trm :: spets) vars (mk_conj (mk_imp (a, b), mk_imp (b, a)))
     else
-      let
-        val (trm',ctxt2',var) = skolem_var ctxt2 x
-      in
-        (ctxt1,ctxt2',spets,trm',var::vars)
-      end
-
-fun skolemize' pos ctxt1 ctxt2 spets vars (Const (@{const_name Not},_) $ trm') =
-    let
-      val (ctxt1',ctxt2',spets',trm'') = skolemize' (not pos) ctxt1 ctxt2 spets vars trm'
-    in
-      (ctxt1',ctxt2',map mk_not spets',mk_not trm'')
-    end
-  | skolemize' pos ctxt1 ctxt2 spets vars (trm as (Const (@{const_name HOL.eq},t) $ a $ b)) =
-    if contains_quantor trm andalso t = @{typ "bool \<Rightarrow> bool \<Rightarrow> bool"}then
-      skolemize' pos ctxt1 ctxt2 (trm::spets) vars (mk_conj (mk_imp (a,b), mk_imp (b,a)))
-    else
-      (ctxt1,ctxt2,spets,trm)
-  | skolemize' pos ctxt1 ctxt2 spets vars (trm as (Const (name,_) $ Abs x)) =
+      (ctxt1, ctxt2, spets, trm)
+  | skolemize' pos ctxt1 ctxt2 spets vars (trm as (Const (name, _) $ Abs x)) =
     if name = @{const_name Ex} orelse name = @{const_name All} then
       let
         val is_free =  (name = @{const_name Ex} andalso pos) 
           orelse (name = @{const_name All} andalso not pos)
-        val (ctxt1',ctxt2',spets',trm',vars') = 
+        val (ctxt1', ctxt2', spets', trm', vars') = 
           skolem_bound is_free ctxt1 ctxt2 (if is_free then trm :: spets else spets) vars x
       in
         skolemize' pos ctxt1' ctxt2' spets' vars' trm'
       end
     else
-      (ctxt1,ctxt2,spets,trm)
-  | skolemize' pos ctxt1 ctxt2 spets vars ((c as Const (name,_)) $ a $ b) =
+      (ctxt1, ctxt2, spets, trm)
+  | skolemize' pos ctxt1 ctxt2 spets vars ((c as Const (name, _)) $ a $ b) =
     if name = @{const_name conj} orelse name = @{const_name disj} orelse 
        name = @{const_name implies} then
       let
         val pos_a = if name = @{const_name implies} then not pos else pos
-        val (ctxt1',ctxt2',spets',a') = skolemize'  pos_a ctxt1 ctxt2 [] vars a
-        val (ctxt1'',ctxt2'',spets'',b') = skolemize' pos ctxt1' ctxt2' [] vars b
+        val (ctxt1', ctxt2', spets', a') = skolemize'  pos_a ctxt1 ctxt2 [] vars a
+        val (ctxt1'', ctxt2'', spets'', b') = skolemize' pos ctxt1' ctxt2' [] vars b
       in
-        (ctxt1'',ctxt2'',
+        (ctxt1'', ctxt2'',
          map (fn trm => c $ a' $ trm) spets'' @ map (fn trm => c $ trm $ b) spets' @ spets,
          c $ a' $ b')
       end
     else
       (ctxt1,ctxt2,spets,c $ a $ b)
-  | skolemize' _ ctxt1 ctxt2 spets _ trm = (ctxt1,ctxt2,spets,trm)
+  | skolemize' _ ctxt1 ctxt2 spets _ trm = (ctxt1, ctxt2, spets, trm)
 
   fun skolemize positve ctxt trm = 
     let
-      val (ctxt1,_,spets,skolemized_trm) = skolemize' positve ctxt ctxt [] [] trm
+      val (ctxt1, _, spets, skolemized_trm) = skolemize' positve ctxt ctxt [] [] trm
     in
-        (ctxt1,(trm :: List.rev spets,skolemized_trm))
+        (ctxt1, (trm :: List.rev spets, skolemized_trm))
     end
 
 end;
@@ -152,15 +151,16 @@
 val tfree_prefix = "TFree"
 val tvar_prefix = "TVar"
 
-val identifier_character = not o member (op =) [delimiter,open_paranthesis,close_parathesis]
+val identifier_character = not o member (op =) [delimiter, open_paranthesis, close_parathesis]
 
-fun encode_type (Type (name,types)) = 
-type_prefix ^ open_paranthesis ^ name ^ delimiter ^ 
+fun encode_type (Type (name, types)) = 
+  type_prefix ^ open_paranthesis ^ name ^ delimiter ^ 
   (map encode_type types |> String.concatWith delimiter) ^ close_parathesis
-| encode_type (TFree (name,sorts)) = 
-tfree_prefix ^ open_paranthesis ^ name ^ delimiter ^ (String.concatWith delimiter sorts) ^ delimiter
-| encode_type (TVar ((name,i),sorts)) =
-tvar_prefix ^ open_paranthesis ^ open_paranthesis ^ name ^ delimiter ^ Int.toString i ^ 
+| encode_type (TFree (name, sorts)) = 
+  tfree_prefix ^ open_paranthesis ^ name ^ delimiter ^ (String.concatWith delimiter sorts) ^ 
+  close_parathesis
+| encode_type (TVar ((name, i), sorts)) =
+  tvar_prefix ^ open_paranthesis ^ open_paranthesis ^ name ^ delimiter ^ Int.toString i ^ 
   close_parathesis ^ delimiter ^ (String.concatWith delimiter sorts) ^ close_parathesis
 
 fun encode_types types = (String.concatWith delimiter (map encode_type types))
@@ -168,7 +168,8 @@
 fun parse_identifier x =
   (Scan.many identifier_character >> implode) x
   
-fun parse_star delim scanner x = (Scan.optional (scanner ::: Scan.repeat ($$ delim |-- scanner)) []) x
+fun parse_star delim scanner x = 
+  (Scan.optional (scanner ::: Scan.repeat ($$ delim |-- scanner)) []) x
   
 fun parse_type x = (Scan.this_string type_prefix |-- $$ open_paranthesis |-- parse_identifier --|
   $$ delimiter -- parse_star delimiter parse_any_type --| $$ close_parathesis >> Type) x
@@ -183,20 +184,20 @@
 fun parse_types x = parse_star delimiter parse_any_type x
   
 fun decode_type_string s = Scan.finite Symbol.stopper
-           (Scan.error (!! (fn _ => raise FailureMessage ("unrecognized type encoding" ^
-                                                quote s)) parse_type))  (Symbol.explode s) |> fst
+  (Scan.error (!! (fn _ => raise FailureMessage ("unrecognized type encoding" ^
+  quote s)) parse_type))  (Symbol.explode s) |> fst
 
 fun decode_types s = Scan.finite Symbol.stopper
-           (Scan.error (!! (fn _ => raise FailureMessage ("unrecognized type encoding" ^
-           quote s))) parse_types) (Symbol.explode s) |> fst
+  (Scan.error (!! (fn _ => raise FailureMessage ("unrecognized type encoding" ^
+  quote s))) parse_types) (Symbol.explode s) |> fst
 
 fun encode_const (name,tys) = name ^ delimiter ^ encode_types tys
 
 fun parse_const s = (parse_identifier --| $$ delimiter -- parse_types) s
 
 fun decode_const s = Scan.finite Symbol.stopper
-           (Scan.error (!! (fn _ => raise FailureMessage ("unrecognized const encoding" ^
-           quote s))) parse_const) (Symbol.explode s) |> fst
+  (Scan.error (!! (fn _ => raise FailureMessage ("unrecognized const encoding" ^
+  quote s))) parse_const) (Symbol.explode s) |> fst
 
 end;
 
@@ -229,6 +230,7 @@
 val waldmeister_false = "false"
 val waldmeister_skolemize_rule = "waldmeister_skolemize"
 val lam_lift_waldmeister_prefix = "lambda_wm"
+val waldmeister_apply = "wm_apply"
 
 val factsN = "Relevant facts"
 val helpersN = "Helper facts"
@@ -238,7 +240,7 @@
 val WM_ERROR_MSG = "Waldmeister problem generator failed: "
 
 (*
-Some utilitary functions for translation.
+  Some utilitary functions for translation.
 *)
 
 fun gen_ascii_tuple str = (str, ascii_of str)
@@ -251,23 +253,103 @@
 fun lookup table k = 
   List.find (fn (key, _) => key = k) table
 
+fun dest_list' (f $ t) =
+  let
+    val (function, trms) = dest_list' f
+  in
+    (function, t :: trms)
+  end
+  | dest_list' t = (t,[]);
+
+fun dest_list trm = dest_list' trm ||> List.rev
+
+fun list_update x [] = [x]
+  | list_update (a,b) ((c,d) :: xs) =
+  if a = c andalso b < d then
+    (a,b) :: xs
+  else
+    (c,d) :: list_update (a,b) xs
+
 (*
-Translation from Isabelle theorms and terms to ATP terms.
+  Hiding partial applications in terms
+*)
+
+fun map_minimal_app' info (trm :: trms) =
+    map_minimal_app' (minimal_app' info trm) trms
+  | map_minimal_app' info _ = info
+
+and minimal_app' info (trm as _ $ _) =
+  let
+    val (function, trms) = dest_list trm
+    val info' = map_minimal_app' info trms
+  in
+    case function of 
+      (Const _) => list_update (function, length trms) info' |
+      (Free _) => list_update (function, length trms) info' |
+      _ => info
+  end
+  | minimal_app' info (trm as Const _) =
+   list_update (trm, 0) info
+  | minimal_app' info (trm as Free _) =
+   list_update (trm, 0) info
+  | minimal_app' info _ = info;
+
+fun map_minimal_app trms = map_minimal_app' [] trms
+
+fun mk_waldmeister_app function [] = function
+  | mk_waldmeister_app function (a :: args) = 
+    let
+      val funT = type_of function
+      val argT = type_of a
+      val newT = funT --> argT --> (dest_funT funT |> snd)
+    in
+      mk_waldmeister_app (Const (waldmeister_apply ^ encode_type newT, newT) $ function $ a) args
+    end
+
+fun hide_partial_applications info (trm as (_ $ _)) =
+  let
+    val (function, trms) = dest_list trm
+    val trms' = map (hide_partial_applications info) trms
+  in
+    case function of
+    Var _ =>  mk_waldmeister_app function trms' |
+    _ => 
+      let 
+        val min_args = lookup info function |> the |> snd
+        val args0 = List.take (trms',min_args)
+        val args1 = List.drop (trms',min_args)
+        val function' = list_comb (function,args0)
+      in
+        mk_waldmeister_app function' args1
+      end
+  end
+  | hide_partial_applications _ t = t;
+
+fun remove_waldmeister_app ((c as Const (name, _)) $ x $ y) =
+  if String.isPrefix waldmeister_apply name then
+    remove_waldmeister_app x $ remove_waldmeister_app y
+  else
+    c $ remove_waldmeister_app x $ remove_waldmeister_app y
+  | remove_waldmeister_app (x $ y) = remove_waldmeister_app x $ remove_waldmeister_app y
+  | remove_waldmeister_app x = x
+
+(*
+  Translation from Isabelle theorms and terms to ATP terms.
 *)
 
 fun trm_to_atp'' thy (Const (x, ty)) args =
     let
-      val ty_args = if is_lambda_name x then
-        [] else Sign.const_typargs thy (x,ty)
+      val ty_args = if is_lambda_name x orelse String.isPrefix waldmeister_apply x then
+        [] else Sign.const_typargs thy (x, ty)
     in
-      [ATerm ((gen_ascii_tuple (String.str const_prefix ^ encode_const (x,ty_args)), []), args)]
+      [ATerm ((gen_ascii_tuple (String.str const_prefix ^ encode_const (x, ty_args)), []), args)]
     end
   | trm_to_atp'' _ (Free (x, _)) args = 
     [ATerm ((gen_ascii_tuple (String.str free_prefix ^ x), []), args)]
   | trm_to_atp'' _ (Var ((x, _), _)) args = 
     [ATerm ((gen_ascii_tuple (String.str var_prefix ^ x), []), args)]
   | trm_to_atp'' thy (trm1 $ trm2) args = trm_to_atp'' thy trm1 (trm_to_atp'' thy trm2 [] @ args)
-  | trm_to_atp'' _ trm _ = raise FailureTerm (trm,trm)
+  | trm_to_atp'' _ _ _ = raise FailureMessage (WM_ERROR_MSG ^ "Unexpected term")
 
 fun trm_to_atp' thy trm = trm_to_atp'' thy trm [] |> hd
 
@@ -275,30 +357,27 @@
     ATerm ((("equal", "equal"), []), [trm_to_atp' thy lhs, trm_to_atp' thy rhs])
   | eq_trm_to_atp _ _ = raise FailureMessage (WM_ERROR_MSG ^ "Non-eq term")
 
-fun thm_to_atps thy split_conj prop_term =
-  if split_conj then map (eq_trm_to_atp thy) (prop_term |> HOLogic.dest_conj)
-  else [prop_term |> eq_trm_to_atp thy]
-
 (* Translation from ATP terms to Isabelle terms. *)
 
 fun construct_term thy (name, args) =
   let
     val prefix = String.sub (name, 0)
-    val encoded_name = String.extract(name,1,NONE)
+    val encoded_name = String.extract(name, 1, NONE)
     fun dummy_fun_type () = replicate (length args) dummyT ---> dummyT
   in
     if prefix = const_prefix then
       let
-        val (const_name,ty_args) = decode_const encoded_name
+        val (const_name, ty_args) = if String.isPrefix waldmeister_apply encoded_name then
+          (waldmeister_apply, []) else decode_const encoded_name
         val const_trans_name = 
           if is_lambda_name const_name then
-            lam_lift_waldmeister_prefix ^ 
-            String.extract(const_name,size lam_lifted_poly_prefix,NONE)
+            lam_lift_waldmeister_prefix ^ (* ?? *)
+            String.extract(const_name, size lam_lifted_poly_prefix, NONE)
           else
             const_name
       in
         Const (const_trans_name,
-          if is_lambda_name const_name then
+          if is_lambda_name const_name orelse String.isPrefix waldmeister_apply const_name then
             dummyT
           else
             Sign.const_instance thy (const_name, ty_args))
@@ -310,7 +389,7 @@
       (* Use name instead of encoded_name because Waldmeister renames free variables. *)
     else if name = waldmeister_equals then
       (case args of 
-        [_, _] => eq_const dummyT
+        [_, _] => eq_const @{typ bool}
       | _ => raise FailureMessage 
         (WM_ERROR_MSG ^ "waldmeister equals needs 2 arguments but has " ^ 
          Int.toString (length args)))
@@ -337,15 +416,16 @@
 fun formula_to_trm thy (AAtom aterm) = aterm |> atp_to_trm thy
   | formula_to_trm thy (AConn (ANot, [aterm])) =
     mk_not (formula_to_trm thy aterm)
-  | formula_to_trm _ _ = raise FailureMessage (WM_ERROR_MSG ^ "formula_to_trm expects AAtom or AConn")
+  | formula_to_trm _ _ = 
+    raise FailureMessage (WM_ERROR_MSG ^ "formula_to_trm expects AAtom or AConn")
 
 (* Abstract translation *)
 
 fun mk_formula prefix_name name atype aterm =
   Formula ((prefix_name ^ ascii_of name, name), atype, AAtom aterm, NONE, [])
 
-fun problem_lines_of_fact thy prefix (s,(_,(_,t))) =
-  map (mk_formula prefix s Axiom) (thm_to_atps thy false t)
+fun problem_lines_of_fact thy prefix (s, (_, (_, t))) fact_number =
+  mk_formula (prefix ^ Int.toString fact_number ^ "_") s Axiom (eq_trm_to_atp thy t)
 
 fun make_nice problem = nice_atp_problem true CNF problem
 
@@ -364,72 +444,75 @@
 
     val conditions = map preproc hyps_t0
     val consequence = preproc concl_t0
-    (*val hyp_ts = map preproc hyp_ts0 : term list *)
     val facts = map (apsnd preproc #> apfst fst) facts0 : (string * term) list
-    
-    fun map_ctxt' _ ctxt [] ys = (ctxt,ys)
+
+    fun map_ctxt' _ ctxt [] ys = (ctxt, ys)
       | map_ctxt' f ctxt (x :: xs) ys =
         let
-          val (ctxt',x') = f ctxt x
+          val (ctxt', x') = f ctxt x
         in
-          map_ctxt' f ctxt' xs (x'::ys)
+          map_ctxt' f ctxt' xs (x' :: ys)
         end
 
     fun map_ctxt f ctxt xs = map_ctxt' f ctxt xs []
       
-    fun skolemize_fact ctxt (name,trm) = 
+    fun skolemize_fact ctxt (name, trm) = 
       let 
-        val (ctxt',(steps,trm')) = skolemize true ctxt trm 
+        val (ctxt', (steps, trm')) = skolemize true ctxt trm 
       in 
-        (ctxt',(name,(steps,trm')))
+        (ctxt', (name, (steps, trm')))
       end
-    
+
     fun name_list' _ [] _ = []
-      | name_list' prefix (x :: xs) i = (prefix ^ Int.toString i,x) :: name_list' prefix xs (i+1)
-      
-    fun name_list prefix xs = name_list' prefix xs 0 
+      | name_list' prefix (x :: xs) i = (prefix ^ Int.toString i, x) :: name_list' prefix xs (i + 1)
 
-    val (ctxt',sko_facts) = map_ctxt skolemize_fact ctxt facts : 
-      Proof.context * (string * (term list * term)) list
-    val (ctxt'',sko_conditions) = map_ctxt (skolemize true) ctxt' conditions : 
-      Proof.context * (term list * term) list
+    fun name_list prefix xs = name_list' prefix xs 0
+
+    val (ctxt', sko_facts) = map_ctxt skolemize_fact ctxt facts
+    val (ctxt'', sko_conditions) = map_ctxt (skolemize true) ctxt' conditions
 
     val post_skolem = do_cheaply_conceal_lambdas []
 
-    val sko_eq_facts = map (apsnd (apsnd (mk_eq_true #> apsnd post_skolem))) sko_facts : 
-      (string * (term list * (term option * term))) list
-    val sko_eq_conditions = map (apsnd (mk_eq_true #> apsnd post_skolem)) sko_conditions 
-            |> name_list conjecture_condition_name : 
-      (string * (term list * (term option * term))) list
-    val (_,eq_conseq as (_,(non_eq_consequence,eq_consequence))) = 
-      skolemize false ctxt'' consequence |> apsnd (apsnd (mk_eq_true #> apsnd post_skolem)) :
-      (Proof.context * (term list * (term option * term)))
+    val sko_eq_facts0 = map (apsnd (apsnd (mk_eq_true #> apsnd post_skolem))) sko_facts
+    val sko_eq_conditions0 = map (apsnd (mk_eq_true #> apsnd post_skolem)) sko_conditions
+      |> name_list conjecture_condition_name
+    val (_, eq_conseq as (_, (non_eq_consequence0, eq_consequence0))) =
+      skolemize false ctxt'' consequence |> apsnd (apsnd (mk_eq_true #> apsnd post_skolem))
 
     val sko_eq_info =
-      (((conj_identifier,eq_conseq) :: sko_eq_conditions) @ map (apfst (fn name => fact_prefix ^ "0_" ^ name)) sko_eq_facts) : 
-      (string * (term list * (term option * term))) list
+      (((conj_identifier, eq_conseq) :: sko_eq_conditions0) 
+      @ map (apfst (fn name => fact_prefix ^ "0_" ^ name)) sko_eq_facts0)
+
+    val fun_app_info = map_minimal_app (map (snd o snd o snd) sko_eq_info)
+
+    fun hide_partial_apps_in_last (x, (y, (z, term))) = 
+      (x, (y, (z, hide_partial_applications fun_app_info term)))
 
-    val fact_lines = maps (problem_lines_of_fact thy (fact_prefix ^ "0_" (* FIXME *))) sko_eq_facts
+    val sko_eq_facts = map hide_partial_apps_in_last sko_eq_facts0
+    val sko_eq_conditions = map hide_partial_apps_in_last sko_eq_conditions0
+    val eq_consequence = hide_partial_applications fun_app_info eq_consequence0
+
+    fun map_enum _ _ [] = []
+      | map_enum f i (x :: xs) = f x i :: map_enum f (i + 1) xs
+
+    val fact_lines = map_enum (problem_lines_of_fact thy fact_prefix) 0 sko_eq_facts
     val condition_lines =
-      map (fn (name,(_,(_,trm))) => mk_formula fact_prefix name Hypothesis (eq_trm_to_atp thy trm)) sko_eq_conditions
+      map (fn (name, (_, (_, trm))) =>
+        mk_formula fact_prefix name Hypothesis (eq_trm_to_atp thy trm)) sko_eq_conditions
     val axiom_lines = fact_lines @ condition_lines
 
     val conj_line = mk_conjecture (eq_trm_to_atp thy eq_consequence)
-    
-    fun is_some (SOME _) = true
-      | is_some NONE = false
-    
+
     val helper_lemmas_needed = List.exists (snd #> snd #> fst #> is_some) sko_eq_facts
       orelse List.exists (snd #> snd #> fst #> is_some) sko_eq_conditions orelse
-      is_some non_eq_consequence
+      is_some non_eq_consequence0
 
     val helper_lines =
       if helper_lemmas_needed then
         [(helpersN,
           @{thms waldmeister_fol}
           |> map (fn th => (("", (Global, General)), preproc (prop_of th)))
-          |> maps 
-            (fn ((s,_),t) => map (mk_formula helper_prefix s Axiom) (thm_to_atps thy false t)))]
+          |> map (fn ((s, _) ,t) => mk_formula helper_prefix s Axiom (eq_trm_to_atp thy t)))]
       else
         []
 
@@ -443,7 +526,7 @@
 fun termify_line ctxt (name, role, u, rule, deps) =
   let
     val thy = Proof_Context.theory_of ctxt
-    val t = u |> formula_to_trm thy
+    val t = u |> formula_to_trm thy |> remove_waldmeister_app
       |> singleton (infer_formulas_types ctxt)
       |> HOLogic.mk_Trueprop
   in
@@ -455,43 +538,53 @@
   #> map (termify_line ctxt)
   #> repair_waldmeister_endgame
 
-
 fun get_skolem_info info names = case map (lookup info) names |> List.find is_some of
   SOME x => x |
   NONE => NONE
   
-fun fix_name name = 
-  if String.isPrefix "fact" name then 
+fun fix_name name = (* fixme *)
+  if String.isPrefix fact_prefix name then 
     String.extract(name,7,NONE) |> unascii_of |> curry (op ^) "fact_0_"
   else
     name
 
-fun skolemization_steps info 
-  (proof_step as ((waldmeister_name,isabelle_names), role, trm, rule, _)) =
+fun skolemization_steps info
+  (proof_step as ((waldmeister_name, isabelle_names), _, trm, rule, _)) =
   case get_skolem_info info (map fix_name isabelle_names) of
     NONE => [proof_step] |
-    SOME (_,([],_)) => [proof_step] |
-    SOME (_,(step :: steps,_)) =>
+    SOME (_, ([], _)) => [proof_step] |
+    SOME (_, (step :: steps,_)) =>
       let
-        val is_conjecture = String.isPrefix "1.0.0.0" waldmeister_name
-
-        fun mk_steps _ [] = []
-          | mk_steps i (x :: xs) = (((waldmeister_name ^ "_" ^  Int.toString i),[]),Plain,
-            mk_Trueprop (if is_conjecture then mk_not x else x),waldmeister_skolemize_rule,
-            [(waldmeister_name ^ "_" ^  Int.toString (i-1),if i = 1 then isabelle_names else [])]) 
-            :: mk_steps (i+1) xs
-        val skolem_steps = ((waldmeister_name ^ "_0",isabelle_names),Unknown,
-            mk_Trueprop (if is_conjecture then mk_not step else step),rule,[]) :: 
-          mk_steps 1 steps
+        val raw_trm = dest_Trueprop trm
+        val is_narrowing = raw_trm = @{term "True = False"} orelse raw_trm = @{term "False = True"}
+        val is_conjecture = String.isPrefix "1.0.0.0" waldmeister_name andalso not is_narrowing
       in
-        if role = Conjecture then
+        if is_narrowing then
           [proof_step]
         else
-          skolem_steps @ [((waldmeister_name,[]), Unknown, trm, waldmeister_skolemize_rule,
-            [(waldmeister_name ^ "_" ^ Int.toString (length skolem_steps - 1),if length skolem_steps = 1 then isabelle_names else [])])]
+          let
+            fun mk_steps _ [] = []
+              | mk_steps i (x :: xs) = (((waldmeister_name ^ "_" ^  Int.toString i),[]),
+                Plain, mk_Trueprop ((is_conjecture ? mk_not) x), waldmeister_skolemize_rule,
+                [(waldmeister_name ^ "_" ^  Int.toString (i-1),
+                    if i = 1 then isabelle_names else [])]) 
+                :: mk_steps (i+1) xs
+
+            val first_step = ((waldmeister_name ^ "_0", isabelle_names), Unknown,
+                mk_Trueprop ((is_conjecture ? mk_not) step), rule, [])
+
+            val sub_steps =  mk_steps 1 steps
+
+            val skolem_steps = first_step :: sub_steps
+            val num_of_steps = length skolem_steps
+          in
+            (skolem_steps @ 
+            [((waldmeister_name, []), Unknown, trm, waldmeister_skolemize_rule,
+            [(waldmeister_name ^ "_" ^ Int.toString (num_of_steps - 1),
+                if num_of_steps = 1 then isabelle_names else [])])])
+          end
       end
   
-fun introduce_waldmeister_skolems info (proof_steps : (term, string) atp_step list) = proof_steps
+fun introduce_waldmeister_skolems info proof_steps = proof_steps
       |> map (skolemization_steps info) |> List.concat
-
 end;