# HG changeset patch
# User berghofe
# Date 1175777770 -7200
# Node ID 962f824c2df9a75ebe98cde9a625c005c8fc1522
# Parent  41b092e7d89ac43b5e76396e8cb2eae2b261c713
- Tried to make name_of_thm more robust against changes of the
  structure of proofs.
- Now uses add_inductive_global rather than add_inductive_i for
  the definition of the realizability predicate.

diff -r 41b092e7d89a -r 962f824c2df9 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Thu Apr 05 14:51:28 2007 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Thu Apr 05 14:56:10 2007 +0200
@@ -16,10 +16,10 @@
 struct
 
 (* FIXME: LocalTheory.note should return theorems with proper names! *)
-fun name_of_thm thm = (case Proofterm.strip_combt (fst (Proofterm.strip_combP
-    (Proofterm.rewrite_proof (theory_of_thm thm) ([], []) (proof_of thm)))) of
-    (PThm (name, _, _, _), _) => name
-  | _ => error "name_of_thm: bad proof");
+fun name_of_thm thm =
+  (case Symtab.dest (Proofterm.thms_of_proof' (proof_of thm) Symtab.empty) of
+     [(name, _)] => name
+   | _ => error ("name_of_thm: bad proof of theorem\n" ^ string_of_thm thm));
 
 (* infer order of variables in intro rules from order of quantifiers in elim rule *)
 fun infer_intro_vars elim arity intros =
@@ -397,13 +397,11 @@
     (** realizability predicate **)
 
     val (ind_info, thy3') = thy2 |>
-      TheoryTarget.init NONE |>
-      InductivePackage.add_inductive_i false "" false false false
+      InductivePackage.add_inductive_global false "" false false false
         rlzpreds rlzparams (map (fn (rintr, intr) =>
           ((Sign.base_name (name_of_thm intr), []),
            subst_atomic rlzpreds' (Logic.unvarify rintr)))
              (rintrs ~~ maps snd rss)) [] ||>
-      ProofContext.theory_of o LocalTheory.exit ||>
       Theory.absolute_path;
     val thy3 = PureThy.hide_thms false
       (map name_of_thm (#intrs ind_info)) thy3';