# HG changeset patch
# User wenzelm
# Date 1003082742 -7200
# Node ID 8d8a87f350d623cedf999a676f55e12c6f4a8284
# Parent  d12864826f4cb7828e8f454b62169424be6f9a6a
use ObjectLogic stuff;

diff -r d12864826f4c -r 8d8a87f350d6 src/Provers/induct_method.ML
--- a/src/Provers/induct_method.ML	Sun Oct 14 20:05:07 2001 +0200
+++ b/src/Provers/induct_method.ML	Sun Oct 14 20:05:42 2001 +0200
@@ -146,7 +146,10 @@
 
 local
 
-val atomize_cterm = Thm.cterm_fun AutoBind.drop_judgment o full_rewrite_cterm Data.atomize;
+fun atomize_cterm ct =
+  Thm.cterm_fun
+    (ObjectLogic.drop_judgment (#sign (Thm.rep_cterm ct))) (full_rewrite_cterm Data.atomize ct);
+
 val atomize_tac = Tactic.rewrite_goal_tac Data.atomize;
 val rulify_cterm = full_rewrite_cterm Data.rulify2 o full_rewrite_cterm Data.rulify1;
 
@@ -155,12 +158,12 @@
   Tactic.rewrite_goal_tac Data.rulify2 THEN'
   Tactic.norm_hhf_tac;
 
-fun rulify_cases cert =
+fun rulify_cases sg cert =
   let
     val ruly = Thm.term_of o rulify_cterm o cert;
     fun ruly_case {fixes, assumes, binds} =
       {fixes = fixes, assumes = map ruly assumes,
-        binds = map (apsnd (apsome (AutoBind.drop_judgment o ruly))) binds};
+        binds = map (apsnd (apsome (ObjectLogic.drop_judgment sg o ruly))) binds};
   in map (apsnd ruly_case) ooo RuleCases.make_raw end;
 
 
@@ -216,7 +219,7 @@
 
     fun prep_rule (th, (cases, n)) =
       Seq.map (rpair (cases, drop (n, facts))) (Method.multi_resolves (take (n, facts)) [th]);
-    val tac = resolveq_cases_tac (rulify_cases cert open_parms) atomize_tac
+    val tac = resolveq_cases_tac (rulify_cases sg cert open_parms) atomize_tac
       (Seq.flat (Seq.map prep_rule ruleq));
   in tac THEN_ALL_NEW_CASES rulify_tac end;