# HG changeset patch
# User wenzelm
# Date 902247724 -7200
# Node ID 99116a9e88f89f977c830e439bc1b29d8ab68704
# Parent  a6167c446b0b63a30a3094d49b00cddab9646a9c
added export: thm -> thm;
exported print_current_goals_default;
locale support;

diff -r a6167c446b0b -r 99116a9e88f8 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Tue Aug 04 18:21:20 1998 +0200
+++ b/src/Pure/goals.ML	Tue Aug 04 18:22:04 1998 +0200
@@ -9,7 +9,6 @@
 pending proofs.
 *)
 
-
 signature GOALS =
   sig
   type proof
@@ -29,6 +28,7 @@
   val byev		: tactic list -> unit
   val chop		: unit -> unit
   val choplev		: int -> unit
+  val export            : thm -> thm
   val fa		: unit -> unit
   val fd		: thm -> unit
   val fds		: thm list -> unit
@@ -42,6 +42,7 @@
   val goal		: theory -> string -> thm list
   val goalw		: theory -> thm list -> string -> thm list
   val goalw_cterm	: thm list -> cterm -> thm list
+  val print_current_goals_default: (int -> int -> thm -> unit)
   val print_current_goals_fn : (int -> int -> thm -> unit) ref
   val pop_proof		: unit -> thm list
   val pr		: unit -> unit
@@ -82,6 +83,7 @@
 
 datatype proof = Proof of gstack list * thm list * (bool*thm->thm);
 
+
 (*** References ***)
 
 (*Should process time be printed after proof steps?*)
@@ -128,6 +130,21 @@
 
 val result_error_fn = ref result_error_default;
 
+(* alternative to standard: this function does not discharge the hypotheses
+   first. Is used for locales, in the following function prepare_proof *)
+fun varify th =
+  let val {maxidx,...} = rep_thm th
+  in
+    th |> forall_intr_frees |> forall_elim_vars (maxidx + 1)
+       |> Thm.strip_shyps |> Thm.implies_intr_shyps
+       |> zero_var_indexes |> Thm.varifyT |> Thm.compress
+  end;
+
+(** exporting a theorem out of a locale means turning all meta-hyps into assumptions
+    and expand and cancel the locale definitions. It's relatively easy, because 
+    a definiendum is a locale const, hence Free, hence Var, after standard **)
+val export = standard o Seq.hd o (REPEAT (FIRSTGOAL (rtac reflexive_thm))) o standard;
+
 (*Common treatment of "goal" and "prove_goal":
   Return assumptions, initial proof state, and function to make result.
   "atomic" indicates if the goal should be wrapped up in the function
@@ -160,7 +177,8 @@
 		 sign_error (sign,sign'))
             else if ngoals>0 then !result_error_fn state
 		(string_of_int ngoals ^ " unsolved goals!")
-            else if not (null hyps) then !result_error_fn state
+            else if (not (null hyps) andalso (not (Locale.in_locale hyps sign)))
+		 then !result_error_fn state
                 ("Additional hypotheses:\n" ^ 
                  cat_lines (map (Sign.string_of_term sign) hyps))
 	    else if not (null xshyps) then !result_error_fn state
@@ -168,7 +186,8 @@
                  commas (map (Sign.str_of_sort sign) xshyps))
 	    else if Pattern.matches (#tsig(Sign.rep_sg sign)) 
 			            (term_of chorn, prop)
-		 then  standard th
+		 then  (if (null(hyps)) then standard th 
+                       else varify th)
 	    else  !result_error_fn state "proved a different theorem"
         end
   in
@@ -328,9 +347,9 @@
 
 (*Version taking the goal as a string*)
 fun agoalw atomic thy rths agoal = 
-  agoalw_cterm atomic rths (read_cterm(sign_of thy)(agoal,propT))
-  handle ERROR => error (*from type_assign, etc via prepare_proof*)
-	    ("The error(s) above occurred for " ^ quote agoal);
+    agoalw_cterm atomic rths (Locale.read_cterm(sign_of thy)(agoal,propT))
+    handle ERROR => error (*from type_assign, etc via prepare_proof*)
+	("The error(s) above occurred for " ^ quote agoal);
 
 val goalw = agoalw false;
 
@@ -499,4 +518,6 @@
 
 end;
 
+
+
 open Goals;