src/Pure/Isar/obtain.ML
changeset 18678 dd0c569fa43d
parent 18670 c3f445b92aff
child 18693 8ae076ee5e19
     1.1 --- a/src/Pure/Isar/obtain.ML	Fri Jan 13 17:39:41 2006 +0100
     1.2 +++ b/src/Pure/Isar/obtain.ML	Sat Jan 14 17:14:06 2006 +0100
     1.3 @@ -52,7 +52,7 @@
     1.4  
     1.5  (** obtain_export **)
     1.6  
     1.7 -fun obtain_export state parms rule cprops thm =
     1.8 +fun obtain_export ctxt parms rule cprops thm =
     1.9    let
    1.10      val {thy, prop, maxidx, ...} = Thm.rep_thm thm;
    1.11      val cparms = map (Thm.cterm_of thy) parms;
    1.12 @@ -67,10 +67,10 @@
    1.13      val bads = parms inter (Term.term_frees concl);
    1.14    in
    1.15      if not (null bads) then
    1.16 -      raise Proof.STATE ("Conclusion contains obtained parameters: " ^
    1.17 -        space_implode " " (map (ProofContext.string_of_term (Proof.context_of state)) bads), state)
    1.18 +      error ("Conclusion contains obtained parameters: " ^
    1.19 +        space_implode " " (map (ProofContext.string_of_term ctxt) bads))
    1.20      else if not (ObjectLogic.is_judgment thy concl) then
    1.21 -      raise Proof.STATE ("Conclusion in obtained context must be object-logic judgments", state)
    1.22 +      error "Conclusion in obtained context must be object-logic judgments"
    1.23      else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule
    1.24    end;
    1.25  
    1.26 @@ -92,6 +92,7 @@
    1.27    let
    1.28      val _ = Proof.assert_forward_or_chain state;
    1.29      val ctxt = Proof.context_of state;
    1.30 +    val thy = Proof.theory_of state;
    1.31      val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
    1.32  
    1.33      (*obtain vars*)
    1.34 @@ -103,7 +104,7 @@
    1.35      (*obtain asms*)
    1.36      val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
    1.37      val asm_props = List.concat (map (map fst) proppss);
    1.38 -    val asms = map fst (Attrib.map_specs (prep_att (Proof.theory_of state)) raw_asms) ~~ proppss;
    1.39 +    val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss;
    1.40  
    1.41      val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt;
    1.42  
    1.43 @@ -129,7 +130,7 @@
    1.44        Proof.local_qed (NONE, false)
    1.45        #> Seq.map (`Proof.the_fact #-> (fn rule =>
    1.46          Proof.fix_i (xs ~~ Ts)
    1.47 -        #> Proof.assm_i (K (obtain_export state parms rule)) asms));
    1.48 +        #> Proof.assm_i (K (obtain_export ctxt parms rule)) asms));
    1.49    in
    1.50      state
    1.51      |> Proof.enter_forward
    1.52 @@ -157,14 +158,13 @@
    1.53  
    1.54  local
    1.55  
    1.56 -fun match_params state vars rule =
    1.57 +fun match_params ctxt vars rule =
    1.58    let
    1.59 -    val ctxt = Proof.context_of state;
    1.60 -    val thy = Proof.theory_of state;
    1.61 +    val thy = ProofContext.theory_of ctxt;
    1.62      val string_of_typ = ProofContext.string_of_typ ctxt;
    1.63      val string_of_term = setmp show_types true (ProofContext.string_of_term ctxt);
    1.64  
    1.65 -    fun err msg th = raise Proof.STATE (msg ^ ":\n" ^ ProofContext.string_of_thm ctxt th, state);
    1.66 +    fun err msg th = error (msg ^ ":\n" ^ ProofContext.string_of_thm ctxt th);
    1.67  
    1.68      val params = RuleCases.strip_params (Logic.nth_prem (1, Thm.prop_of rule));
    1.69      val m = length vars;
    1.70 @@ -214,26 +214,23 @@
    1.71          [prem] =>
    1.72            if Thm.concl_of th aconv thesis andalso
    1.73              Logic.strip_assums_concl prem aconv thesis then ()
    1.74 -          else raise Proof.STATE ("Guessed a different clause:\n" ^
    1.75 -            ProofContext.string_of_thm ctxt th, state)
    1.76 -      | [] => raise Proof.STATE ("Goal solved -- nothing guessed.", state)
    1.77 -      | _ => raise Proof.STATE ("Guess split into several cases:\n" ^
    1.78 -        ProofContext.string_of_thm ctxt th, state));
    1.79 +          else error ("Guessed a different clause:\n" ^ ProofContext.string_of_thm ctxt th)
    1.80 +      | [] => error "Goal solved -- nothing guessed."
    1.81 +      | _ => error ("Guess split into several cases:\n" ^ ProofContext.string_of_thm ctxt th));
    1.82  
    1.83      fun guess_context raw_rule =
    1.84        let
    1.85 -        val (parms, rule) = match_params state (map (fn (x, T, _) => (x, T)) vars) raw_rule;
    1.86 +        val (parms, rule) = match_params ctxt (map (fn (x, T, _) => (x, T)) vars) raw_rule;
    1.87          val (bind, _) = ProofContext.bind_fixes (map #1 parms) ctxt;
    1.88          val ts = map (bind o Free) parms;
    1.89          val ps = map dest_Free ts;
    1.90          val asms =
    1.91            Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule))
    1.92            |> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), ([], [])));
    1.93 -        val _ = conditional (null asms) (fn () =>
    1.94 -          raise Proof.STATE ("Trivial result -- nothing guessed", state));
    1.95 +        val _ = conditional (null asms) (fn () => error "Trivial result -- nothing guessed");
    1.96        in
    1.97          Proof.fix_i (map (apsnd SOME) parms)
    1.98 -        #> Proof.assm_i (K (obtain_export state ts rule)) [(("", []), asms)]
    1.99 +        #> Proof.assm_i (K (obtain_export ctxt ts rule)) [(("", []), asms)]
   1.100          #> Proof.add_binds_i AutoBind.no_facts
   1.101        end;
   1.102