Fixed bug in the handling of congruence rules

--- a/src/HOL/Tools/function_package/context_tree.ML	Mon Oct 23 16:56:35 2006 +0200
+++ b/src/HOL/Tools/function_package/context_tree.ML	Mon Oct 23 17:46:11 2006 +0200
@@ -16,7 +16,7 @@
     val add_congs : thm list
 
     val mk_tree: (thm * FundefCommon.depgraph) list ->
-                 (string * typ) -> Proof.context -> term -> FundefCommon.ctx_tree
+                 (string * typ) -> term -> Proof.context -> term -> FundefCommon.ctx_tree
 
     val inst_tree: theory -> term -> term -> FundefCommon.ctx_tree
                    -> FundefCommon.ctx_tree
@@ -83,34 +83,38 @@
       (ctx', fixes, assumes, rhs_of term)
     end
 
-fun find_cong_rule ctx ((r,dep)::rs) t =
+fun find_cong_rule ctx fvar h ((r,dep)::rs) t =
     (let
-	val (c, subs) = (meta_rhs_of (concl_of r), prems_of r)
+       val thy = ProofContext.theory_of ctx
+       val r = print (zero_var_indexes r)
 
-	val subst = Pattern.match (ProofContext.theory_of ctx) (c, t) (Vartab.empty, Vartab.empty)
+       val tt' = Logic.mk_equals (Pattern.rewrite_term thy [(Free fvar, h)] [] t, t)
+       val (c, subs) = (concl_of r, prems_of r)
 
-	val branches = map (mk_branch ctx o Envir.beta_norm o Envir.subst_vars subst) subs
+       val subst = Pattern.match (ProofContext.theory_of ctx) (c, tt') (Vartab.empty, Vartab.empty)
+       val branches = map (mk_branch ctx o Envir.beta_norm o Envir.subst_vars subst) subs
+       val inst = map (fn v => (cterm_of thy (Var v), cterm_of thy (Envir.subst_vars subst (Var v)))) (Term.add_vars c [])
      in
-	 (r, dep, branches)
+	 (cterm_instantiate inst r, dep, branches)
      end
-    handle Pattern.MATCH => find_cong_rule ctx rs t)
-  | find_cong_rule _ [] _ = sys_error "function_package/context_tree.ML: No cong rule found!"
+    handle Pattern.MATCH => find_cong_rule ctx fvar h rs t)
+  | find_cong_rule _ _ _ [] _ = sys_error "function_package/context_tree.ML: No cong rule found!"
 
 
 fun matchcall fvar (a $ b) = if a = Free fvar then SOME b else NONE
   | matchcall fvar _ = NONE
 
-fun mk_tree congs fvar ctx t =
+fun mk_tree congs fvar h ctx t =
     case matchcall fvar t of
-      SOME arg => RCall (t, mk_tree congs fvar ctx arg)
+      SOME arg => RCall (t, mk_tree congs fvar h ctx arg)
     | NONE => 
       if not (exists_subterm (fn Free v => v = fvar | _ => false) t) then Leaf t
       else 
-	let val (r, dep, branches) = find_cong_rule ctx congs t in
+	let val (r, dep, branches) = find_cong_rule ctx fvar h congs t in
 	  Cong (t, r, dep, 
                 map (fn (ctx', fixes, assumes, st) => 
 			(fixes, map (assume o cterm_of (ProofContext.theory_of ctx)) assumes, 
-                         mk_tree congs fvar ctx' st)) branches)
+                         mk_tree congs fvar h ctx' st)) branches)
 	end
 		
 

--- a/src/HOL/Tools/function_package/fundef_prep.ML	Mon Oct 23 16:56:35 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_prep.ML	Mon Oct 23 17:46:11 2006 +0200
@@ -495,7 +495,7 @@
       val congs = get_fundef_congs (Context.Proof lthy)
       val (globals, ctxt') = fix_globals domT ranT fvar lthy
 
-      val Globals { x, ... } = globals
+      val Globals { x, h, ... } = globals
 
       val clauses = map (mk_clause_context x ctxt') abstract_qglrs 
 
@@ -504,7 +504,7 @@
       val congs_deps = map (fn c => (c, FundefCtxTree.cong_deps c)) (congs @ FundefCtxTree.add_congs) (* FIXME: Save in theory *)
               
       fun build_tree (ClauseContext { ctxt, rhs, ...}) = 
-            FundefCtxTree.mk_tree congs_deps (fname, fT) ctxt rhs
+            FundefCtxTree.mk_tree congs_deps (fname, fT) h ctxt rhs
 
       val trees = map build_tree clauses
       val RCss = map find_calls trees