tuned;
authorwenzelm
Tue Jun 06 20:42:28 2006 +0200 (2006-06-06)
changeset 1979894f12468bbba
parent 19797 a527b3e1076a
child 19799 666de5708ae8
tuned;
src/HOL/OrderedGroup.thy
src/HOL/Tools/rewrite_hol_proof.ML
src/Provers/Arith/abel_cancel.ML
src/Pure/Isar/attrib.ML
src/Pure/meta_simplifier.ML
     1.1 --- a/src/HOL/OrderedGroup.thy	Tue Jun 06 20:42:27 2006 +0200
     1.2 +++ b/src/HOL/OrderedGroup.thy	Tue Jun 06 20:42:28 2006 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  
     1.5  theory OrderedGroup
     1.6  imports Inductive LOrder
     1.7 -uses "../Provers/Arith/abel_cancel.ML"
     1.8 +uses "~~/src/Provers/Arith/abel_cancel.ML"
     1.9  begin
    1.10  
    1.11  text {*
     2.1 --- a/src/HOL/Tools/rewrite_hol_proof.ML	Tue Jun 06 20:42:27 2006 +0200
     2.2 +++ b/src/HOL/Tools/rewrite_hol_proof.ML	Tue Jun 06 20:42:28 2006 +0200
     2.3 @@ -103,7 +103,7 @@
     2.4   \  (allI % TYPE('a) % P %%  \
     2.5   \    (Lam x.  \
     2.6   \        iffD2 % P x % Q x %% (prf % x) %%  \
     2.7 - \         (spec % TYPE('a) % ?Q % x %% prf')))",
     2.8 + \         (spec % TYPE('a) % Q % x %% prf')))",
     2.9  
    2.10     (* Ex *)
    2.11  
     3.1 --- a/src/Provers/Arith/abel_cancel.ML	Tue Jun 06 20:42:27 2006 +0200
     3.2 +++ b/src/Provers/Arith/abel_cancel.ML	Tue Jun 06 20:42:28 2006 +0200
     3.3 @@ -118,7 +118,7 @@
     3.4     handle Cancel => NONE;
     3.5  
     3.6   val rel_conv =
     3.7 -     Simplifier.simproc_i (Theory.deref thy_ref) "cancel_relations"
     3.8 -       (map Data.dest_eqI eqI_rules) rel_proc;
     3.9 +     Simplifier.mk_simproc "cancel_relations"
    3.10 +       (map (Thm.cterm_of (Theory.deref thy_ref) o Data.dest_eqI) eqI_rules) rel_proc;
    3.11  
    3.12  end;
     4.1 --- a/src/Pure/Isar/attrib.ML	Tue Jun 06 20:42:27 2006 +0200
     4.2 +++ b/src/Pure/Isar/attrib.ML	Tue Jun 06 20:42:28 2006 +0200
     4.3 @@ -244,10 +244,10 @@
     4.4  
     4.5  in
     4.6  
     4.7 -fun read_instantiate mixed_insts (generic, thm) =
     4.8 +fun read_instantiate mixed_insts (context, thm) =
     4.9    let
    4.10 -    val thy = Context.theory_of generic;
    4.11 -    val ctxt = Context.proof_of generic;
    4.12 +    val thy = Context.theory_of context;
    4.13 +    val ctxt = Context.proof_of context;
    4.14  
    4.15      val (type_insts, term_insts) = List.partition (is_tvar o fst) (map snd mixed_insts);
    4.16      val internal_insts = term_insts |> map_filter
    4.17 @@ -316,7 +316,7 @@
    4.18          else
    4.19            Args.assign (SOME (Args.Term (the (AList.lookup (op =) term_insts''' xi)))) arg);
    4.20  
    4.21 -  in (generic, thm''' |> RuleCases.save thm) end;
    4.22 +  in (context, thm''' |> RuleCases.save thm) end;
    4.23  
    4.24  end;
    4.25  
    4.26 @@ -344,7 +344,7 @@
    4.27  
    4.28  local
    4.29  
    4.30 -fun read_instantiate' (args, concl_args) (generic, thm) =
    4.31 +fun read_instantiate' (args, concl_args) (context, thm) =
    4.32    let
    4.33      fun zip_vars _ [] = []
    4.34        | zip_vars (_ :: xs) ((_, NONE) :: rest) = zip_vars xs rest
    4.35 @@ -353,7 +353,7 @@
    4.36      val insts =
    4.37        zip_vars (Drule.vars_of_terms [Thm.prop_of thm]) args @
    4.38        zip_vars (Drule.vars_of_terms [Thm.concl_of thm]) concl_args;
    4.39 -  in read_instantiate insts (generic, thm) end;
    4.40 +  in read_instantiate insts (context, thm) end;
    4.41  
    4.42  val value =
    4.43    Args.internal_term >> Args.Term ||
     5.1 --- a/src/Pure/meta_simplifier.ML	Tue Jun 06 20:42:27 2006 +0200
     5.2 +++ b/src/Pure/meta_simplifier.ML	Tue Jun 06 20:42:28 2006 +0200
     5.3 @@ -332,6 +332,7 @@
     5.4        Proc {name = name, lhs = lhs, proc = proc, id = id}))
     5.5    end;
     5.6  
     5.7 +(* FIXME avoid global thy and Logic.varify *)
     5.8  fun simproc_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify);
     5.9  fun simproc thy name = simproc_i thy name o map (Sign.read_term thy);
    5.10