# HG changeset patch
# User wenzelm
# Date 965047038 -7200
# Node ID b16624f1ea385d2cf7d4da2be775964fd4f6882a
# Parent  7afb808b6b3ecafa1832c353ec861298287141c2
tuned;

diff -r 7afb808b6b3e -r b16624f1ea38 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Jul 31 14:33:40 2000 +0200
+++ b/src/HOL/IsaMakefile	Mon Jul 31 14:37:18 2000 +0200
@@ -498,16 +498,18 @@
 ## clean
 
 clean:
-	@rm -f $(OUT)/HOL $(OUT)/HOL-Real $(LOG)/HOL.gz $(LOG)/HOL-Subst.gz \
-	  $(LOG)/HOL-IMP.gz $(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz \
-	  $(LOG)/HOL-Induct.gz $(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \
-	  $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
-	  $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
-	  $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz $(LOG)/HOL-BCV.gz $(LOG)/HOL-IOA.gz \
-	  $(LOG)/HOL-AxClasses-Group.gz		\
-	  $(LOG)/HOL-AxClasses-Lattice.gz	\
-	  $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz \
-	  $(LOG)/HOL-ex.gz $(LOG)/HOL-Isar_examples.gz $(OUT)/TLA \
-	  $(LOG)/TLA.gz $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz \
-	  $(LOG)/TLA-Memory.gz $(LOG)/HOL-Real.gz $(LOG)/HOL-Real-ex.gz \
-	  $(LOG)/HOL-Real-HahnBanach.gz
+	@rm -f $(OUT)/HOL $(OUT)/HOL-Real $(OUT)/TLA \
+		$(LOG)/HOL.gz $(LOG)/HOL-Real.gz $(LOG)/TLA.gz \
+		$(LOG)/HOL-Isar_examples.gz $(LOG)/HOL-Induct.gz \
+		$(LOG)/HOL-ex.gz $(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz \
+		$(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz \
+		$(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \
+		$(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
+		$(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
+		$(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \
+		$(LOG)/HOL-BCV.gz $(LOG)/HOL-MicroJava.gz \
+		$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses-Group.gz \
+		$(LOG)/HOL-AxClasses-Lattice.gz	\
+		$(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Real-ex.gz \
+		$(LOG)/HOL-Real-HahnBanach.gz $(LOG)/TLA-Inc.gz \
+		$(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz
diff -r 7afb808b6b3e -r b16624f1ea38 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Mon Jul 31 14:33:40 2000 +0200
+++ b/src/Pure/Isar/obtain.ML	Mon Jul 31 14:37:18 2000 +0200
@@ -38,7 +38,7 @@
 struct
 
 
-(** export_obtained **)
+(** disch_obtained **)
 
 fun disch_obtained state parms rule cprops thm =
   let
@@ -55,16 +55,13 @@
     val bads = parms inter (Term.term_frees concl);
   in
     if not (null bads) then
-      raise Proof.STATE ("Result contains illegal parameters: " ^
+      raise Proof.STATE ("Conclusion contains obtained parameters: " ^
         space_implode " " (map (Sign.string_of_term sign) bads), state)
     else if not (AutoBind.is_judgment (Logic.strip_assums_concl prop)) then
-      raise Proof.STATE ("Conclusion of result is not an object-logic judgment", state)
+      raise Proof.STATE ("Conclusion is not an object-logic judgment", state)
     else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule
   end;
 
-fun export_obtained state parms rule =
-  (disch_obtained state parms rule, fn _ => fn _ => []);
-
 
 
 (** obtain(_i) **)
@@ -108,11 +105,14 @@
     val bound_thesis = bind_skolem (Data.atomic_thesis thesisN);
     val that_prop = Term.list_all_free (xs', Logic.list_implies (asm_props, bound_thesis));
 
+    fun export_obtained rule =
+      (disch_obtained state parms rule, fn _ => fn _ => []);
+
     fun after_qed st = st
       |> Proof.end_block
       |> Seq.map (fn st' => st'
         |> Proof.fix_i vars
-        |> Proof.assm_i (export_obtained state parms (Proof.the_fact st')) asms);
+        |> Proof.assm_i (export_obtained (Proof.the_fact st')) asms);
   in
     state
     |> Proof.enter_forward