- Tried to make name_of_thm more robust against changes of the
authorberghofe
Thu Apr 05 14:56:10 2007 +0200 (2007-04-05)
changeset 22606962f824c2df9
parent 22605 41b092e7d89a
child 22607 760b9351bcf7
- 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.
src/HOL/Tools/inductive_realizer.ML
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Thu Apr 05 14:51:28 2007 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu Apr 05 14:56:10 2007 +0200
     1.3 @@ -16,10 +16,10 @@
     1.4  struct
     1.5  
     1.6  (* FIXME: LocalTheory.note should return theorems with proper names! *)
     1.7 -fun name_of_thm thm = (case Proofterm.strip_combt (fst (Proofterm.strip_combP
     1.8 -    (Proofterm.rewrite_proof (theory_of_thm thm) ([], []) (proof_of thm)))) of
     1.9 -    (PThm (name, _, _, _), _) => name
    1.10 -  | _ => error "name_of_thm: bad proof");
    1.11 +fun name_of_thm thm =
    1.12 +  (case Symtab.dest (Proofterm.thms_of_proof' (proof_of thm) Symtab.empty) of
    1.13 +     [(name, _)] => name
    1.14 +   | _ => error ("name_of_thm: bad proof of theorem\n" ^ string_of_thm thm));
    1.15  
    1.16  (* infer order of variables in intro rules from order of quantifiers in elim rule *)
    1.17  fun infer_intro_vars elim arity intros =
    1.18 @@ -397,13 +397,11 @@
    1.19      (** realizability predicate **)
    1.20  
    1.21      val (ind_info, thy3') = thy2 |>
    1.22 -      TheoryTarget.init NONE |>
    1.23 -      InductivePackage.add_inductive_i false "" false false false
    1.24 +      InductivePackage.add_inductive_global false "" false false false
    1.25          rlzpreds rlzparams (map (fn (rintr, intr) =>
    1.26            ((Sign.base_name (name_of_thm intr), []),
    1.27             subst_atomic rlzpreds' (Logic.unvarify rintr)))
    1.28               (rintrs ~~ maps snd rss)) [] ||>
    1.29 -      ProofContext.theory_of o LocalTheory.exit ||>
    1.30        Theory.absolute_path;
    1.31      val thy3 = PureThy.hide_thms false
    1.32        (map name_of_thm (#intrs ind_info)) thy3';