src/HOL/Tools/BNF/bnf_gfp.ML
changeset 59621 291934bac95e
parent 59580 cbc38731d42f
child 59819 dbec7f33093d
     1.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -1080,7 +1080,7 @@
     1.4          val goal = list_all_free (kl :: zs)
     1.5            (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs));
     1.6  
     1.7 -        val cts = map (SOME o Proof_Context.cterm_of lthy) [Term.absfree nat' goal, nat];
     1.8 +        val cts = map (SOME o Thm.cterm_of lthy) [Term.absfree nat' goal, nat];
     1.9  
    1.10          val length_Lev =
    1.11            Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
    1.12 @@ -1115,8 +1115,8 @@
    1.13              Library.foldr1 HOLogic.mk_conj
    1.14                (map2 (mk_conjunct i z) ks zs_copy)) ks zs));
    1.15  
    1.16 -        val cTs = [SOME (Proof_Context.ctyp_of lthy sum_sbdT)];
    1.17 -        val cts = map (SOME o Proof_Context.cterm_of lthy) [Term.absfree kl' goal, kl];
    1.18 +        val cTs = [SOME (Thm.ctyp_of lthy sum_sbdT)];
    1.19 +        val cts = map (SOME o Thm.cterm_of lthy) [Term.absfree kl' goal, kl];
    1.20  
    1.21          val rv_last =
    1.22            Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
    1.23 @@ -1153,7 +1153,7 @@
    1.24          val goal = list_all_free (kl :: zs @ zs_copy @ zs_copy2)
    1.25            (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs));
    1.26  
    1.27 -        val cts = map (SOME o Proof_Context.cterm_of lthy) [Term.absfree nat' goal, nat];
    1.28 +        val cts = map (SOME o Thm.cterm_of lthy) [Term.absfree nat' goal, nat];
    1.29  
    1.30          val set_Lev =
    1.31            Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
    1.32 @@ -1192,7 +1192,7 @@
    1.33          val goal = list_all_free (kl :: k :: zs @ zs_copy)
    1.34            (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs));
    1.35  
    1.36 -        val cts = map (SOME o Proof_Context.cterm_of lthy) [Term.absfree nat' goal, nat];
    1.37 +        val cts = map (SOME o Thm.cterm_of lthy) [Term.absfree nat' goal, nat];
    1.38  
    1.39          val set_image_Lev =
    1.40            Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
    1.41 @@ -1867,7 +1867,7 @@
    1.42                    Logic.list_implies (prems, HOLogic.mk_Trueprop concl)) premss concls
    1.43  
    1.44                  val ctss =
    1.45 -                  map (fn phi => map (SOME o Proof_Context.cterm_of lthy) [Term.absfree nat' phi, nat]) concls;
    1.46 +                  map (fn phi => map (SOME o Thm.cterm_of lthy) [Term.absfree nat' phi, nat]) concls;
    1.47                in
    1.48                  @{map 4} (fn goal => fn cts => fn col_0s => fn col_Sucs =>
    1.49                    Goal.prove_sorry lthy [] [] goal
    1.50 @@ -1952,10 +1952,10 @@
    1.51                maps (map (fn thm => thm RS @{thm subset_Collect_iff})) dtor_Jset_incl_thmss @
    1.52                  @{thms subset_Collect_iff[OF subset_refl]};
    1.53  
    1.54 -            val cTs = map (SOME o Proof_Context.ctyp_of lthy) params';
    1.55 +            val cTs = map (SOME o Thm.ctyp_of lthy) params';
    1.56              fun mk_induct_tinst phis jsets y y' =
    1.57                @{map 4} (fn phi => fn jset => fn Jz => fn Jz' =>
    1.58 -                SOME (Proof_Context.cterm_of lthy (Term.absfree Jz' (HOLogic.mk_Collect (fst y', snd y',
    1.59 +                SOME (Thm.cterm_of lthy (Term.absfree Jz' (HOLogic.mk_Collect (fst y', snd y',
    1.60                    HOLogic.mk_conj (HOLogic.mk_mem (y, jset $ Jz), phi $ y $ Jz))))))
    1.61                phis jsets Jzs Jzs';
    1.62            in
    1.63 @@ -2024,7 +2024,7 @@
    1.64              val goals = @{map 3} mk_goal fs colss colss';
    1.65  
    1.66              val ctss =
    1.67 -              map (fn phi => map (SOME o Proof_Context.cterm_of lthy) [Term.absfree nat' phi, nat]) goals;
    1.68 +              map (fn phi => map (SOME o Thm.cterm_of lthy) [Term.absfree nat' phi, nat]) goals;
    1.69  
    1.70              val thms =
    1.71                @{map 4} (fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
    1.72 @@ -2047,7 +2047,7 @@
    1.73  
    1.74              val goals = map (mk_goal Jbds) colss;
    1.75  
    1.76 -            val ctss = map (fn phi => map (SOME o Proof_Context.cterm_of lthy) [Term.absfree nat' phi, nat])
    1.77 +            val ctss = map (fn phi => map (SOME o Thm.cterm_of lthy) [Term.absfree nat' phi, nat])
    1.78                (map (mk_goal (replicate n sbd)) colss);
    1.79  
    1.80              val thms =
    1.81 @@ -2064,7 +2064,7 @@
    1.82  
    1.83          val map_cong0_thms =
    1.84            let
    1.85 -            val cTs = map (SOME o Proof_Context.ctyp_of lthy o
    1.86 +            val cTs = map (SOME o Thm.ctyp_of lthy o
    1.87                Term.typ_subst_atomic (passiveAs ~~ passiveBs) o TFree) coinduct_params;
    1.88  
    1.89              fun mk_prem z set f g y y' =
    1.90 @@ -2086,7 +2086,7 @@
    1.91                HOLogic.mk_exists (x, T, mk_coind_body sets z' z fmap gmap y y_copy)
    1.92                |> Term.absfree y'_copy
    1.93                |> Term.absfree y'
    1.94 -              |> Proof_Context.cterm_of lthy;
    1.95 +              |> Thm.cterm_of lthy;
    1.96  
    1.97              val cphis = @{map 9} mk_cphi
    1.98                Jsetss_by_bnf Jzs' Jzs fs_Jmaps fs_copy_Jmaps Jys' Jys Jys'_copy Jys_copy;
    1.99 @@ -2189,9 +2189,9 @@
   1.100                activeJphis Jzs Jz's_copy Jz's Jmap_snds zip_unfolds;
   1.101            fun mk_cts zs z's phis =
   1.102              @{map 3} (fn z => fn z' => fn phi =>
   1.103 -              SOME (Proof_Context.cterm_of lthy (fold_rev (Term.absfree o Term.dest_Free) [z', z] phi)))
   1.104 +              SOME (Thm.cterm_of lthy (fold_rev (Term.absfree o Term.dest_Free) [z', z] phi)))
   1.105              zs z's phis @
   1.106 -            map (SOME o Proof_Context.cterm_of lthy) (splice z's zs);
   1.107 +            map (SOME o Thm.cterm_of lthy) (splice z's zs);
   1.108            val cts1 = mk_cts Jzs Jzs_copy coind1_phis;
   1.109            val cts2 = mk_cts Jz's Jz's_copy coind2_phis;
   1.110  
   1.111 @@ -2228,9 +2228,9 @@
   1.112              Jphis abs fstABs sndABs;
   1.113            val ctss = map2 (fn ab' => fn phis =>
   1.114                map2 (fn z' => fn phi =>
   1.115 -                SOME (Proof_Context.cterm_of lthy (Term.absfree ab' (Term.absfree z' phi))))
   1.116 +                SOME (Thm.cterm_of lthy (Term.absfree ab' (Term.absfree z' phi))))
   1.117                zip_zs' phis @
   1.118 -              map (SOME o Proof_Context.cterm_of lthy) zip_zs)
   1.119 +              map (SOME o Thm.cterm_of lthy) zip_zs)
   1.120              abs' helper_ind_phiss;
   1.121            fun mk_helper_ind_concl ab' z ind_phi set =
   1.122              mk_Ball (set $ z) (Term.absfree ab' ind_phi);