# HG changeset patch
# User ballarin
# Date 1064934350 -7200
# Node ID a15951091d5d3688216ff987da7f43fce4dacf53
# Parent  ebf291f3b449df8ecfebdd5c0dbd1c85ca6b7fdd
Removed garbage accidentally left behind in file.

diff -r ebf291f3b449 -r a15951091d5d src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Sep 30 15:13:02 2003 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Sep 30 17:05:50 2003 +0200
@@ -888,7 +888,7 @@
       activate_facts prep_facts ((context, axioms), ps);
 
 (* CB: testing *)
-
+(*
 val axioms' = if true (* null axioms *) then axioms' else
 let val {view = (ax3_view, ax3_axioms), ...} =
   the_locale (ProofContext.theory_of context) "Type.ax3";
@@ -897,6 +897,7 @@
 val {view = (ax4_view, ax4_axioms), ...} =
   the_locale (ProofContext.theory_of context) "Type.ax4";
 in axioms' @ ax3_axioms @ [ax_TrueFalse] @ (tl ax4_axioms) end;
+*)
     val ((ctxt, _), (elemss, _)) =
       activate_facts prep_facts ((import_ctxt, axioms'), qs);
   in
@@ -922,29 +923,12 @@
 
 in
 
-(* CB
-arguments are (see below): x->import, y->body (elements?), z->context
+(* CB: arguments are: x->import, y->body (elements?), z->context *)
 fun read_context x y z = #1 (gen_context true [] [] x y [] z);
 fun cert_context x y z = #1 (gen_context_i true [] [] x y [] z);
-*)
-fun read_context x y z = (warning "read_context\n"; #1 (gen_context true [] [] x y [] z));
-fun cert_context x y z = (warning "cert_context\n"; #1 (gen_context_i true [] [] x y [] z));
 
-(* CB
 val read_context_statement = gen_statement intern gen_context;
 val cert_context_statement = gen_statement (K I) gen_context_i;
-*)
-
-fun read_context_statement so cs xss ctxt =
-let val (locale, view_statement, locale_ctxt, elems_ctxt, concl') =
-  gen_statement intern gen_context so cs xss ctxt;
-in (locale, view_statement, locale_ctxt, elems_ctxt, concl')
-end;
-fun cert_context_statement so cs xss ctxt =
-let val (locale, view_statement, locale_ctxt, elems_ctxt, concl') =
-  gen_statement (K I) gen_context_i so cs xss ctxt;
-in (locale, view_statement, locale_ctxt, elems_ctxt, concl')  
-end;
 
 end;