# HG changeset patch
# User paulson
# Date 1151597459 -7200
# Node ID 806eaa2a2a5e6ea67f0bfdfe7b6b242bacab0ecb
# Parent  016ba2d907a7b33b80f2323d398f13a3e95bea21
fixed the "factor" method

diff -r 016ba2d907a7 -r 806eaa2a2a5e src/HOL/Tools/reconstruction.ML
--- a/src/HOL/Tools/reconstruction.ML	Thu Jun 29 13:53:05 2006 +0200
+++ b/src/HOL/Tools/reconstruction.ML	Thu Jun 29 18:10:59 2006 +0200
@@ -9,18 +9,6 @@
 structure Reconstruction =
 struct
 
-(**************************************************************)
-(* extra functions necessary for factoring and paramodulation *)
-(**************************************************************)
-
-fun mksubstlist [] sublist = sublist
-  | mksubstlist ((a, (_, b)) :: rest) sublist =
-      let val vartype = type_of b
-          val avar = Var(a,vartype)
-          val newlist = ((avar,b)::sublist)
-      in mksubstlist rest newlist end;
-
-
 (**** attributes ****)
 
 (** Binary resolution **)
@@ -34,21 +22,26 @@
     >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => binary_rule ((A, i), (B, j)))));
 
 
-fun inst_single sign t1 t2 cl =
-    let val ct1 = cterm_of sign t1 and ct2 = cterm_of sign t2
-    in  hd (Seq.list_of(distinct_subgoals_tac
-                            (cterm_instantiate [(ct1,ct2)] cl)))
-    end;
+(** Factoring **)
+
+(*NB this code did not work at all before 29/6/2006. Even now its behaviour may
+  not be as expected. It unifies the designated literals
+  and then deletes ALL duplicates of literals (not just those designated)*)
+
+fun mksubstlist [] sublist = sublist
+  | mksubstlist ((a, (T, b)) :: rest) sublist =
+      mksubstlist rest ((Var(a,T), b)::sublist);
 
-fun inst_subst sign substs cl =
-    if (is_Var (fst(hd(substs))))
-    then inst_single sign (fst (hd substs)) (snd (hd substs)) cl
-    else if (is_Var (snd(hd(substs))))
-    then inst_single sign (snd (hd substs)) (fst (hd substs)) cl
-    else raise THM ("inst_subst", 0, [cl]);
+fun reorient (x,y) = 
+      if is_Var x then (x,y)
+      else if is_Var y then (y,x)
+      else error "Reconstruction.reorient: neither term is a Var";
 
-
-(** Factoring **)
+fun inst_subst sign subst cl =
+  let val subst' = map (pairself (cterm_of sign) o reorient) subst
+  in 
+      Seq.hd(distinct_subgoals_tac (cterm_instantiate subst' cl))
+  end;
 
 fun factor_rule (cl, lit1, lit2) =
     let