src/HOL/Tools/inductive_realizer.ML
changeset 30435 e62d6ecab6ad
parent 30364 577edc39b501
child 30528 7173bf123335
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed Mar 11 15:38:25 2009 +0100
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Wed Mar 11 15:42:19 2009 +0100
     1.3 @@ -355,7 +355,7 @@
     1.4            ((Binding.name (Long_Name.base_name (name_of_thm intr)), []),
     1.5             subst_atomic rlzpreds' (Logic.unvarify rintr)))
     1.6               (rintrs ~~ maps snd rss)) [] ||>
     1.7 -      Sign.absolute_path;
     1.8 +      Sign.root_path;
     1.9      val thy3 = fold (PureThy.hide_fact false o name_of_thm) (#intrs ind_info) thy3';
    1.10  
    1.11      (** realizer for induction rule **)
    1.12 @@ -394,12 +394,12 @@
    1.13             REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
    1.14               [K (rewrite_goals_tac rews), ObjectLogic.atomize_prems_tac,
    1.15                DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
    1.16 -        val (thm', thy') = PureThy.store_thm (Binding.name (space_implode "_"
    1.17 +        val (thm', thy') = PureThy.store_thm (Binding.qualified_name (space_implode "_"
    1.18            (Long_Name.qualify qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy;
    1.19          val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
    1.20            (DatatypeAux.split_conj_thm thm');
    1.21          val ([thms'], thy'') = PureThy.add_thmss
    1.22 -          [((Binding.name (space_implode "_"
    1.23 +          [((Binding.qualified_name (space_implode "_"
    1.24               (Long_Name.qualify qualifier "inducts" :: vs' @ Ps @
    1.25                 ["correctness"])), thms), [])] thy';
    1.26          val realizers = inducts ~~ thms' ~~ rlzs ~~ rs;
    1.27 @@ -454,7 +454,7 @@
    1.28             rewrite_goals_tac rews,
    1.29             REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_prems_tac THEN'
    1.30               DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
    1.31 -        val (thm', thy') = PureThy.store_thm (Binding.name (space_implode "_"
    1.32 +        val (thm', thy') = PureThy.store_thm (Binding.qualified_name (space_implode "_"
    1.33            (name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy
    1.34        in
    1.35          Extraction.add_realizers_i