# HG changeset patch
# User berghofe
# Date 1170846528 -3600
# Node ID 159bfab776e2aa472a71533a0ff4bd52b54efb70
# Parent  23f3ca04d3b30e3dfdffc0ec235de1b9caca25ab
"prove" function now instantiates relation variable in order
to avoid problems with higher-order unification. This allows
relations to be encoded as binary predicates.

diff -r 23f3ca04d3b3 -r 159bfab776e2 src/Provers/trancl.ML
--- a/src/Provers/trancl.ML	Wed Feb 07 12:05:54 2007 +0100
+++ b/src/Provers/trancl.ML	Wed Feb 07 12:08:48 2007 +0100
@@ -81,15 +81,19 @@
 struct
 
  
- datatype proof
+datatype proof
   = Asm of int 
   | Thm of proof list * thm; 
 
- exception Cannot; (* internal exception: raised if no proof can be found *)
+exception Cannot; (* internal exception: raised if no proof can be found *)
 
- fun prove asms = 
-  let fun pr (Asm i) = List.nth (asms, i)
-  |       pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
+fun prove thy r asms = 
+  let
+    fun inst thm =
+      let val SOME (_, _, r', _) = Cls.decomp (concl_of thm)
+      in Drule.cterm_instantiate [(cterm_of thy r', cterm_of thy r)] thm end;
+    fun pr (Asm i) = List.nth (asms, i)
+      | pr (Thm (prfs, thm)) = map pr prfs MRS inst thm
   in pr end;
 
   
@@ -525,8 +529,9 @@
 end;
  
    
-val trancl_tac =   SUBGOAL (fn (A, n) =>
+val trancl_tac =   SUBGOAL (fn (A, n) => fn st =>
  let
+  val thy = theory_of_thm st;
   val Hs = Logic.strip_assums_hyp A;
   val C = Logic.strip_assums_concl A;
   val (rel,subgoals, prf) = mkconcl_trancl C;
@@ -535,15 +540,16 @@
 
  in
   METAHYPS (fn asms =>
-    let val thms = map (prove asms) prfs
-    in rtac (prove thms prf) 1 end) n
+    let val thms = map (prove thy rel asms) prfs
+    in rtac (prove thy rel thms prf) 1 end) n st
  end
-handle  Cannot  => no_tac);
+handle  Cannot  => no_tac st);
 
  
  
-val rtrancl_tac =   SUBGOAL (fn (A, n) =>
+val rtrancl_tac =   SUBGOAL (fn (A, n) => fn st =>
  let
+  val thy = theory_of_thm st;
   val Hs = Logic.strip_assums_hyp A;
   val C = Logic.strip_assums_concl A;
   val (rel,subgoals, prf) = mkconcl_rtrancl C;
@@ -552,9 +558,9 @@
   val prfs = solveRtrancl (prems, C);
  in
   METAHYPS (fn asms =>
-    let val thms = map (prove asms) prfs
-    in rtac (prove thms prf) 1 end) n
+    let val thms = map (prove thy rel asms) prfs
+    in rtac (prove thy rel thms prf) 1 end) n st
  end
-handle  Cannot  => no_tac);
+handle  Cannot  => no_tac st);
 
 end;