# HG changeset patch
# User paulson
# Date 1192114299 -7200
# Node ID a2f15968a6f2a2069d0623525dea6f6427508bff
# Parent  dc67846b00c0a8bddc521bc8211eebd4c1dfc0b9
reconstruction bug fix

diff -r dc67846b00c0 -r a2f15968a6f2 src/HOL/Tools/metis_tools.ML
--- a/src/HOL/Tools/metis_tools.ML	Thu Oct 11 16:38:57 2007 +0200
+++ b/src/HOL/Tools/metis_tools.ML	Thu Oct 11 16:51:39 2007 +0200
@@ -24,8 +24,7 @@
   (* ------------------------------------------------------------------------- *)
   (* Useful Theorems                                                           *)
   (* ------------------------------------------------------------------------- *)
-  val EXCLUDED_MIDDLE' = read_instantiate [("R","False")] notE;
-  val EXCLUDED_MIDDLE  = rotate_prems 1 EXCLUDED_MIDDLE';
+  val EXCLUDED_MIDDLE  = rotate_prems 1 (read_instantiate [("R","False")] notE);
   val REFL_THM         = incr_indexes 2 (Meson.make_meta_clause refl);  (*Rename from 0,1*)
   val subst_em  = zero_var_indexes (subst RS EXCLUDED_MIDDLE);
   val ssubst_em  = read_instantiate [("t","?s"),("s","?t")] (sym RS subst_em);
@@ -278,7 +277,9 @@
 
   fun is_TrueI th = Thm.eq_thm(TrueI,th);
 
-fun inst_excluded_middle th thy i_atm =
+  fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx));
+
+  fun inst_excluded_middle th thy i_atm =
     let val vx = hd (term_vars (prop_of th))
         val substs = [(cterm_of thy vx, cterm_of thy i_atm)]
     in  cterm_instantiate substs th  end;
@@ -319,7 +320,7 @@
         val substs = List.mapPartial remove_typeinst (Metis.Subst.toList fsubst)
         val (vars,rawtms) = ListPair.unzip (List.mapPartial subst_translation substs)
         val tms = infer_types ctxt rawtms;
-        val ctm_of = cterm_of thy o (map_types o Logic.incr_tvar) (1 + Thm.maxidx_of i_th)
+        val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
         val substs' = ListPair.zip (vars, map ctm_of tms)
         val _ = Output.debug (fn() => "subst_translations:")
         val _ = app (fn (x,y) => Output.debug (fn () => string_of_cterm x ^ " |-> " ^
@@ -366,11 +367,15 @@
     end;
 
   (* INFERENCE RULE: REFL *)
-  fun refl_inf ctxt lit =
+  val refl_x = cterm_of @{theory} (hd (term_vars (prop_of REFL_THM)));
+  val refl_idx = 1 + Thm.maxidx_of REFL_THM;
+  
+  fun refl_inf ctxt t =
     let val thy = ProofContext.theory_of ctxt
-        val v_x = hd (term_vars (prop_of REFL_THM))
-        val i_lit = singleton (fol_terms_to_hol ctxt) lit
-    in  cterm_instantiate [(cterm_of thy v_x, cterm_of thy i_lit)] REFL_THM  end;
+        val i_t = singleton (fol_terms_to_hol ctxt) t
+        val _ = Output.debug (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
+        val c_t = cterm_incr_types thy refl_idx i_t
+    in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
 
   fun get_ty_arg_size thy (Const("op =",_)) = 0  (*equality has no type arguments*)
     | get_ty_arg_size thy (Const(c,_))      = (Recon.num_typargs thy c handle TYPE _ => 0)