simplified ObjectLogic.atomize;
authorwenzelm
Thu Jul 05 20:01:28 2007 +0200 (2007-07-05)
changeset 23591d32a85385e17
parent 23590 ad95084a5c63
child 23592 ba0912262b2c
simplified ObjectLogic.atomize;
src/HOL/Library/EfficientNat.thy
src/HOL/Nominal/nominal_induct.ML
src/HOL/Tools/specification_package.ML
src/Provers/blast.ML
src/Provers/induct_method.ML
src/Pure/Isar/locale.ML
     1.1 --- a/src/HOL/Library/EfficientNat.thy	Thu Jul 05 20:01:26 2007 +0200
     1.2 +++ b/src/HOL/Library/EfficientNat.thy	Thu Jul 05 20:01:28 2007 +0200
     1.3 @@ -336,7 +336,7 @@
     1.4        | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
     1.5        | find_var _ = NONE;
     1.6      fun find_thm th =
     1.7 -      let val th' = ObjectLogic.atomize_thm th
     1.8 +      let val th' = Conv.fconv_rule ObjectLogic.atomize th
     1.9        in Option.map (pair (th, th')) (find_var (prop_of th')) end
    1.10    in
    1.11      case get_first find_thm thms of
     2.1 --- a/src/HOL/Nominal/nominal_induct.ML	Thu Jul 05 20:01:26 2007 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Thu Jul 05 20:01:28 2007 +0200
     2.3 @@ -88,7 +88,7 @@
     2.4      val cert = Thm.cterm_of thy;
     2.5  
     2.6      val ((insts, defs), defs_ctxt) = fold_map InductMethod.add_defs def_insts ctxt |>> split_list;
     2.7 -    val atomized_defs = map (map ObjectLogic.atomize_thm) defs;
     2.8 +    val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs;
     2.9  
    2.10      val finish_rule =
    2.11        split_all_tuples
     3.1 --- a/src/HOL/Tools/specification_package.ML	Thu Jul 05 20:01:26 2007 +0200
     3.2 +++ b/src/HOL/Tools/specification_package.ML	Thu Jul 05 20:01:28 2007 +0200
     3.3 @@ -121,7 +121,7 @@
     3.4            | myfoldr f [] = error "SpecificationPackage.process_spec internal error"
     3.5  
     3.6          val rew_imps = alt_props |>
     3.7 -          map (ObjectLogic.atomize_cterm o Thm.read_cterm thy o rpair Term.propT o snd)
     3.8 +          map (ObjectLogic.atomize o Thm.read_cterm thy o rpair Term.propT o snd)
     3.9          val props' = rew_imps |>
    3.10            map (HOLogic.dest_Trueprop o term_of o snd o Thm.dest_equals o cprop_of)
    3.11  
     4.1 --- a/src/Provers/blast.ML	Thu Jul 05 20:01:26 2007 +0200
     4.2 +++ b/src/Provers/blast.ML	Thu Jul 05 20:01:28 2007 +0200
     4.3 @@ -1247,7 +1247,7 @@
     4.4          (also prints reconstruction time)
     4.5   "lim" is depth limit.*)
     4.6  fun timing_depth_tac start cs lim i st0 =
     4.7 -  let val st = (initialize (theory_of_thm st0); ObjectLogic.atomize_goal i st0);
     4.8 +  let val st = (initialize (theory_of_thm st0); Conv.gconv_rule ObjectLogic.atomize_prems i st0);
     4.9        val sign = Thm.theory_of_thm st
    4.10        val skoprem = fromSubgoal (List.nth(prems_of st, i-1))
    4.11        val hyps  = strip_imp_prems skoprem
     5.1 --- a/src/Provers/induct_method.ML	Thu Jul 05 20:01:26 2007 +0200
     5.2 +++ b/src/Provers/induct_method.ML	Thu Jul 05 20:01:28 2007 +0200
     5.3 @@ -363,7 +363,7 @@
     5.4      val cert = Thm.cterm_of thy;
     5.5  
     5.6      val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
     5.7 -    val atomized_defs = map (map ObjectLogic.atomize_thm) defs;
     5.8 +    val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs;
     5.9  
    5.10      fun inst_rule (concls, r) =
    5.11        (if null insts then `RuleCases.get r
     6.1 --- a/src/Pure/Isar/locale.ML	Thu Jul 05 20:01:26 2007 +0200
     6.2 +++ b/src/Pure/Isar/locale.ML	Thu Jul 05 20:01:28 2007 +0200
     6.3 @@ -1692,7 +1692,7 @@
     6.4      val bodyT = Term.fastype_of body;
     6.5    in
     6.6      if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
     6.7 -    else (body, bodyT, ObjectLogic.atomize_cterm (Thm.cterm_of thy t))
     6.8 +    else (body, bodyT, ObjectLogic.atomize (Thm.cterm_of thy t))
     6.9    end;
    6.10  
    6.11  fun aprop_tr' n c = (c, fn args =>