# HG changeset patch
# User wenzelm
# Date 1154287730 -7200
# Node ID 4fe3c0911907e0851c76cf1f2d7e4b5157d1555f
# Parent  ebe183ff903d5a7a01d4e24a87fe9c9704d23b56
demod_rule: depend on context, proper Variable.import/export;

diff -r ebe183ff903d -r 4fe3c0911907 src/HOL/Tools/reconstruction.ML
--- a/src/HOL/Tools/reconstruction.ML	Sun Jul 30 21:28:48 2006 +0200
+++ b/src/HOL/Tools/reconstruction.ML	Sun Jul 30 21:28:50 2006 +0200
@@ -81,18 +81,19 @@
 
 (** Demodulation: rewriting of a single literal (Non-Unit Rewriting, SPASS) **)
 
-fun demod_rule ((cl1, lit1), (cl2 , lit2)) =
+fun demod_rule ctxt ((cl1, lit1), (cl2 , lit2)) =
     let  val eq_lit_th = select_literal (lit1+1) cl1
          val mod_lit_th = select_literal (lit2+1) cl2
-         val (fmod_th,thaw) = Drule.freeze_thaw_robust mod_lit_th
+         val ((_, [fmod_th]), ctxt') = Variable.import true [mod_lit_th] ctxt
          val eqsubst = eq_lit_th RSN (2,rev_subst)
-         val newth = Seq.hd(biresolution false [(false, fmod_th)] 1 eqsubst)
-         val offset = #maxidx(rep_thm newth) + 1
-                          (*ensures "renaming apart" even when Vars are frozen*)
-    in Meson.negated_asm_of_head (thaw offset newth) end;
+         val newth =
+           Seq.hd (biresolution false [(false, fmod_th)] 1 eqsubst)
+           |> singleton (Variable.export ctxt' ctxt)
+    in Meson.negated_asm_of_head newth end;
 
 val demod = Attrib.syntax (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat
-  >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => demod_rule ((A, i), (B, j)))));
+  >> (fn ((i, B), j) => Thm.rule_attribute (fn context => fn A =>
+      demod_rule (Context.proof_of context) ((A, i), (B, j)))));
 
 
 (** Conversion of a theorem into clauses **)