qualified MetaSimplifier.norm_hhf(_protect);
authorwenzelm
Thu Nov 30 14:17:29 2006 +0100 (2006-11-30)
changeset 216054e7307e229b3
parent 21604 1af327306c8e
child 21606 dc75da2cb7d1
qualified MetaSimplifier.norm_hhf(_protect);
src/Pure/Isar/element.ML
src/Pure/Isar/obtain.ML
src/Pure/assumption.ML
src/Pure/meta_simplifier.ML
src/Pure/subgoal.ML
     1.1 --- a/src/Pure/Isar/element.ML	Thu Nov 30 14:17:29 2006 +0100
     1.2 +++ b/src/Pure/Isar/element.ML	Thu Nov 30 14:17:29 2006 +0100
     1.3 @@ -245,7 +245,7 @@
     1.4      val thy = ProofContext.theory_of ctxt;
     1.5      val cert = Thm.cterm_of thy;
     1.6  
     1.7 -    val th = norm_hhf raw_th;
     1.8 +    val th = MetaSimplifier.norm_hhf raw_th;
     1.9      val is_elim = ObjectLogic.is_elim th;
    1.10  
    1.11      val ((_, [th']), ctxt') = Variable.import true [th] ctxt;
    1.12 @@ -291,7 +291,7 @@
    1.13    Witness (t, Goal.prove ctxt [] [] (Logic.protect t) (fn _ =>
    1.14      Tactic.rtac Drule.protectI 1 THEN tac));
    1.15  
    1.16 -fun conclude_witness (Witness (_, th)) = norm_hhf (Goal.conclude th);
    1.17 +fun conclude_witness (Witness (_, th)) = MetaSimplifier.norm_hhf_protect (Goal.conclude th);
    1.18  
    1.19  val mark_witness = Logic.protect;
    1.20  
     2.1 --- a/src/Pure/Isar/obtain.ML	Thu Nov 30 14:17:29 2006 +0100
     2.2 +++ b/src/Pure/Isar/obtain.ML	Thu Nov 30 14:17:29 2006 +0100
     2.3 @@ -187,7 +187,7 @@
     2.4      val rule =
     2.5        (case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) (Goal.init (cert thesis)) of
     2.6          NONE => raise THM ("Obtain.result: tactic failed", 0, facts)
     2.7 -      | SOME th => check_result ctxt thesis (norm_hhf (Goal.conclude th)));
     2.8 +      | SOME th => check_result ctxt thesis (MetaSimplifier.norm_hhf (Goal.conclude th)));
     2.9  
    2.10      val closed_rule = Thm.forall_intr (cert (Free thesis_var)) rule;
    2.11      val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt;
    2.12 @@ -292,7 +292,7 @@
    2.13      val goal = Var (("guess", 0), propT);
    2.14      fun print_result ctxt' (k, [(s, [_, th])]) =
    2.15        ProofDisplay.print_results int ctxt' (k, [(s, [th])]);
    2.16 -    val before_qed = SOME (Method.primitive_text (Goal.conclude #> norm_hhf #>
    2.17 +    val before_qed = SOME (Method.primitive_text (Goal.conclude #> MetaSimplifier.norm_hhf #>
    2.18          (fn th => Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
    2.19      fun after_qed [[_, res]] =
    2.20        Proof.end_block #> guess_context (check_result ctxt thesis res) #> Seq.single;
     3.1 --- a/src/Pure/assumption.ML	Thu Nov 30 14:17:29 2006 +0100
     3.2 +++ b/src/Pure/assumption.ML	Thu Nov 30 14:17:29 2006 +0100
     3.3 @@ -47,7 +47,7 @@
     3.4  *)
     3.5  fun presume_export _ = assume_export false;
     3.6  
     3.7 -val assume = norm_hhf o Thm.assume;
     3.8 +val assume = MetaSimplifier.norm_hhf o Thm.assume;
     3.9  
    3.10  
    3.11  
    3.12 @@ -100,9 +100,9 @@
    3.13  
    3.14  fun export is_goal inner outer =
    3.15    let val asms = Library.drop (length (assumptions_of outer), assumptions_of inner) in
    3.16 -    norm_hhf_protect
    3.17 +    MetaSimplifier.norm_hhf_protect
    3.18      #> fold_rev (fn (e, As) => e is_goal As) asms
    3.19 -    #> norm_hhf_protect
    3.20 +    #> MetaSimplifier.norm_hhf_protect
    3.21    end;
    3.22  
    3.23  fun export_morphism inner outer =
     4.1 --- a/src/Pure/meta_simplifier.ML	Thu Nov 30 14:17:29 2006 +0100
     4.2 +++ b/src/Pure/meta_simplifier.ML	Thu Nov 30 14:17:29 2006 +0100
     4.3 @@ -72,8 +72,6 @@
     4.4    val addSSolver: simpset * solver -> simpset
     4.5    val setSolver: simpset * solver -> simpset
     4.6    val addSolver: simpset * solver -> simpset
     4.7 -  val norm_hhf: thm -> thm
     4.8 -  val norm_hhf_protect: thm -> thm
     4.9  end;
    4.10  
    4.11  signature META_SIMPLIFIER =
    4.12 @@ -104,6 +102,8 @@
    4.13    val rewrite_goals_rule_aux: (simpset -> thm -> thm option) -> thm list -> thm -> thm
    4.14    val rewrite_goal_rule: bool * bool * bool ->
    4.15      (simpset -> thm -> thm option) -> simpset -> int -> thm -> thm
    4.16 +  val norm_hhf: thm -> thm
    4.17 +  val norm_hhf_protect: thm -> thm
    4.18  end;
    4.19  
    4.20  structure MetaSimplifier: META_SIMPLIFIER =
     5.1 --- a/src/Pure/subgoal.ML	Thu Nov 30 14:17:29 2006 +0100
     5.2 +++ b/src/Pure/subgoal.ML	Thu Nov 30 14:17:29 2006 +0100
     5.3 @@ -29,7 +29,8 @@
     5.4  
     5.5  fun focus ctxt i st =
     5.6    let
     5.7 -    val ((schematics, [st']), ctxt') = Variable.import true [norm_hhf st] ctxt;
     5.8 +    val ((schematics, [st']), ctxt') =
     5.9 +      Variable.import true [MetaSimplifier.norm_hhf_protect st] ctxt;
    5.10      val ((params, goal), ctxt'') = Variable.focus_subgoal i st' ctxt';
    5.11      val asms = Drule.strip_imp_prems goal;
    5.12      val concl = Drule.strip_imp_concl goal;