src/Pure/Isar/specification.ML
changeset 29249 4dc278c8dc59
parent 29006 abe0f11cfa4e
child 29581 b3b33e0298eb
     1.1 --- a/src/Pure/Isar/specification.ML	Fri Dec 19 15:05:37 2008 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Fri Dec 19 16:39:23 2008 +0100
     1.3 @@ -59,18 +59,6 @@
     1.4  structure Specification: SPECIFICATION =
     1.5  struct
     1.6  
     1.7 -(* new locales *)
     1.8 -
     1.9 -fun cert_stmt body concl ctxt =
    1.10 -  let val (_, _, ctxt', concl') = Locale.cert_context_statement NONE body concl ctxt
    1.11 -  in (concl', ctxt') end;
    1.12 -fun read_stmt body concl ctxt =
    1.13 -  let val (_, _, ctxt', concl') = Locale.read_context_statement NONE body concl ctxt
    1.14 -  in (concl', ctxt') end;
    1.15 -  
    1.16 -fun cert_context_statement x = if !new_locales then Expression.cert_statement x else cert_stmt x;
    1.17 -fun read_context_statement x = if !new_locales then Expression.read_statement x else read_stmt x;
    1.18 -
    1.19  (* diagnostics *)
    1.20  
    1.21  fun print_consts _ _ [] = ()
    1.22 @@ -370,8 +358,8 @@
    1.23  
    1.24  in
    1.25  
    1.26 -val theorem = gen_theorem (K I) cert_context_statement;
    1.27 -val theorem_cmd = gen_theorem Attrib.intern_src read_context_statement;
    1.28 +val theorem = gen_theorem (K I) Expression.cert_statement;
    1.29 +val theorem_cmd = gen_theorem Attrib.intern_src Expression.read_statement;
    1.30  
    1.31  fun add_theorem_hook f = TheoremHook.map (cons (f, stamp ()));
    1.32