src/Pure/Isar/code.ML
changeset 66128 0181bb24bdca
parent 66127 0561ac527270
child 66129 8a3b141179c2
     1.1 --- a/src/Pure/Isar/code.ML	Tue Jun 20 08:01:56 2017 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Tue Jun 20 08:01:56 2017 +0200
     1.3 @@ -191,9 +191,9 @@
     1.4  
     1.5  datatype spec = Spec of {
     1.6    history_concluded: bool,
     1.7 -  functions: ((bool * fun_spec) * (serial * fun_spec) list) Symtab.table
     1.8 +  types: ((serial * ((string * sort) list * typ_spec)) list) Symtab.table
     1.9      (*with explicit history*),
    1.10 -  types: ((serial * ((string * sort) list * typ_spec)) list) Symtab.table
    1.11 +  functions: ((bool * fun_spec) * (serial * fun_spec) list) Symtab.table
    1.12      (*with explicit history*),
    1.13    cases: ((int * (int * string option list)) * thm) Symtab.table,
    1.14    undefineds: unit Symtab.table
    1.15 @@ -350,7 +350,7 @@
    1.16  
    1.17  (** foundation **)
    1.18  
    1.19 -(* datatypes *)
    1.20 +(* types *)
    1.21  
    1.22  fun no_constr thy s (c, ty) = error ("Not a datatype constructor:\n" ^ string_of_const thy c
    1.23    ^ " :: " ^ string_of_typ thy ty ^ "\n" ^ enclose "(" ")" s);
    1.24 @@ -954,9 +954,11 @@
    1.25       |> cert_of_abs ctxt tyco c;
    1.26  
    1.27  
    1.28 -(* cases *)
    1.29 +(* case certificates *)
    1.30  
    1.31 -fun case_certificate thm =
    1.32 +local
    1.33 +
    1.34 +fun raw_case_cert thm =
    1.35    let
    1.36      val ((head, raw_case_expr), cases) = (apfst Logic.dest_equals
    1.37        o apsnd Logic.dest_conjunctions o Logic.dest_implies o Thm.plain_prop_of) thm;
    1.38 @@ -992,10 +994,14 @@
    1.39        | analyze cases = analyze_cases cases;
    1.40    in (case_const, (n, analyze cases)) end;
    1.41  
    1.42 -fun case_cert thm = case_certificate thm
    1.43 +in
    1.44 +
    1.45 +fun case_cert thm = raw_case_cert thm
    1.46    handle Bind => error "bad case certificate"
    1.47         | TERM _ => error "bad case certificate";
    1.48  
    1.49 +end;
    1.50 +
    1.51  fun get_case_scheme thy =
    1.52    Option.map fst o (Symtab.lookup o the_cases o the_exec) thy;
    1.53  fun get_case_cong thy =