Assumption.assume;
authorwenzelm
Thu Jul 27 13:43:11 2006 +0200 (2006-07-27)
changeset 20233ece639738db3
parent 20232 31998a8c7f25
child 20234 7e0693474bcd
Assumption.assume;
moved Goal.norm_hhf(_protect) to meta_simplifier.ML (pervasive);
src/Pure/Isar/element.ML
     1.1 --- a/src/Pure/Isar/element.ML	Thu Jul 27 13:43:10 2006 +0200
     1.2 +++ b/src/Pure/Isar/element.ML	Thu Jul 27 13:43:11 2006 +0200
     1.3 @@ -120,7 +120,7 @@
     1.4    | prems_of (Defines defs) = map (fst o snd) defs
     1.5    | prems_of _ = [];
     1.6  
     1.7 -fun assume thy t = Goal.norm_hhf (Thm.assume (Thm.cterm_of thy t));
     1.8 +fun assume thy t = Assumption.assume (Thm.cterm_of thy t);
     1.9  
    1.10  fun facts_of thy (Assumes asms) = map (apsnd (map (fn (t, _) => ([assume thy t], [])))) asms
    1.11    | facts_of thy (Defines defs) = map (apsnd (fn (t, _) => [([assume thy t], [])])) defs
    1.12 @@ -228,7 +228,7 @@
    1.13      val thy = ProofContext.theory_of ctxt;
    1.14      val cert = Thm.cterm_of thy;
    1.15  
    1.16 -    val th = Goal.norm_hhf raw_th;
    1.17 +    val th = norm_hhf raw_th;
    1.18      val is_elim = ObjectLogic.is_elim th;
    1.19  
    1.20      val ((_, [th']), ctxt') = Variable.import true [th] ctxt;
    1.21 @@ -272,12 +272,11 @@
    1.22    Witness (t, Goal.prove ctxt [] [] (Logic.protect t) (fn _ =>
    1.23      Tactic.rtac Drule.protectI 1 THEN tac));
    1.24  
    1.25 -fun conclude_witness (Witness (_, th)) = Goal.norm_hhf (Goal.conclude th);
    1.26 +fun conclude_witness (Witness (_, th)) = norm_hhf (Goal.conclude th);
    1.27  
    1.28  val mark_witness = Logic.protect;
    1.29  
    1.30  fun make_witness t th = Witness (t, th);
    1.31 -
    1.32  fun dest_witness (Witness w) = w;
    1.33  
    1.34  fun transfer_witness thy (Witness (t, th)) = Witness (t, Thm.transfer thy th);