src/HOL/Tools/record.ML
changeset 35135 1667fd3b051d
parent 35133 a68e4972fd31
child 35136 34206672b168
     1.1 --- a/src/HOL/Tools/record.ML	Mon Feb 15 20:30:56 2010 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Mon Feb 15 20:32:21 2010 +0100
     1.3 @@ -71,8 +71,7 @@
     1.4  
     1.5  fun named_cterm_instantiate values thm =
     1.6    let
     1.7 -    fun match name ((name', _), _) = name = name'
     1.8 -      | match name _ = false;
     1.9 +    fun match name ((name', _), _) = name = name';
    1.10      fun getvar name =
    1.11        (case find_first (match name) (Term.add_vars (prop_of thm) []) of
    1.12          SOME var => cterm_of (theory_of_thm thm) (Var var)
    1.13 @@ -93,8 +92,8 @@
    1.14    let
    1.15      fun get_thms thy name =
    1.16        let
    1.17 -        val SOME {Rep_inject = rep_inject, Abs_name = absN, abs_type = absT,
    1.18 -          Abs_inverse = abs_inverse, ...} = Typedef.get_info thy name;
    1.19 +        val {Rep_inject = rep_inject, Abs_name = absN, abs_type = absT,
    1.20 +          Abs_inverse = abs_inverse, ...} = Typedef.the_info thy name;
    1.21          val rewrite_rule =
    1.22            MetaSimplifier.rewrite_rule [@{thm iso_tuple_UNIV_I}, @{thm iso_tuple_True_simp}];
    1.23        in
    1.24 @@ -372,7 +371,7 @@
    1.25    equalities: thm Symtab.table,
    1.26    extinjects: thm list,
    1.27    extsplit: thm Symtab.table,  (*maps extension name to split rule*)
    1.28 -  splits: (thm * thm * thm * thm) Symtab.table,  (*!!, !, EX - split-equalities, induct rule*)
    1.29 +  splits: (thm * thm * thm * thm) Symtab.table,  (*!!, ALL, EX - split-equalities, induct rule*)
    1.30    extfields: (string * typ) list Symtab.table,  (*maps extension to its fields*)
    1.31    fieldext: (string * typ list) Symtab.table};  (*maps field to its extension*)
    1.32  
    1.33 @@ -699,7 +698,7 @@
    1.34  fun gen_ext_fields_tr sep mark sfx more ctxt t =
    1.35    let
    1.36      val thy = ProofContext.theory_of ctxt;
    1.37 -    val msg = "error in record input: ";
    1.38 +    fun err msg = raise TERM ("error in record input: " ^ msg, [t]);
    1.39  
    1.40      val fieldargs = dest_ext_fields sep mark t;
    1.41      fun splitargs (field :: fields) ((name, arg) :: fargs) =
    1.42 @@ -707,9 +706,9 @@
    1.43            then
    1.44              let val (args, rest) = splitargs fields fargs
    1.45              in (arg :: args, rest) end
    1.46 -          else raise TERM (msg ^ "expecting field " ^ field ^ " but got " ^ name, [t])
    1.47 +          else err ("expecting field " ^ field ^ " but got " ^ name)
    1.48        | splitargs [] (fargs as (_ :: _)) = ([], fargs)
    1.49 -      | splitargs (_ :: _) [] = raise TERM (msg ^ "expecting more fields", [t])
    1.50 +      | splitargs (_ :: _) [] = err "expecting more fields"
    1.51        | splitargs _ _ = ([], []);
    1.52  
    1.53      fun mk_ext (fargs as (name, _) :: _) =
    1.54 @@ -721,24 +720,24 @@
    1.55                      val (args, rest) = splitargs (map fst (but_last flds)) fargs;
    1.56                      val more' = mk_ext rest;
    1.57                    in list_comb (Syntax.const (suffix sfx ext), args @ [more']) end
    1.58 -              | NONE => raise TERM (msg ^ "no fields defined for " ^ ext, [t]))
    1.59 -          | NONE => raise TERM (msg ^ name ^ " is no proper field", [t]))
    1.60 +              | NONE => err ("no fields defined for " ^ ext))
    1.61 +          | NONE => err (name ^ " is no proper field"))
    1.62        | mk_ext [] = more;
    1.63    in mk_ext fieldargs end;
    1.64  
    1.65  fun gen_ext_type_tr sep mark sfx more ctxt t =
    1.66    let
    1.67      val thy = ProofContext.theory_of ctxt;
    1.68 -    val msg = "error in record-type input: ";
    1.69 +    fun err msg = raise TERM ("error in record-type input: " ^ msg, [t]);
    1.70  
    1.71      val fieldargs = dest_ext_fields sep mark t;
    1.72      fun splitargs (field :: fields) ((name, arg) :: fargs) =
    1.73            if can (unsuffix name) field then
    1.74              let val (args, rest) = splitargs fields fargs
    1.75              in (arg :: args, rest) end
    1.76 -          else raise TERM (msg ^ "expecting field " ^ field ^ " but got " ^ name, [t])
    1.77 +          else err ("expecting field " ^ field ^ " but got " ^ name)
    1.78        | splitargs [] (fargs as (_ :: _)) = ([], fargs)
    1.79 -      | splitargs (_ :: _) [] = raise TERM (msg ^ "expecting more fields", [t])
    1.80 +      | splitargs (_ :: _) [] = err "expecting more fields"
    1.81        | splitargs _ _ = ([], []);
    1.82  
    1.83      fun mk_ext (fargs as (name, _) :: _) =
    1.84 @@ -764,9 +763,9 @@
    1.85                    in
    1.86                      list_comb (Syntax.const (suffix sfx ext), alphas' @ [more'])
    1.87                    end handle Type.TYPE_MATCH =>
    1.88 -                    raise TERM (msg ^ "type is no proper record (extension)", [t]))
    1.89 -              | NONE => raise TERM (msg ^ "no fields defined for " ^ ext, [t]))
    1.90 -          | NONE => raise TERM (msg ^ name ^" is no proper field", [t]))
    1.91 +                    raise err "type is no proper record (extension)")
    1.92 +              | NONE => err ("no fields defined for " ^ ext))
    1.93 +          | NONE => err (name ^ " is no proper field"))
    1.94        | mk_ext [] = more;
    1.95  
    1.96    in mk_ext fieldargs end;
    1.97 @@ -1516,7 +1515,7 @@
    1.98  
    1.99  (* record_split_tac *)
   1.100  
   1.101 -(*Split all records in the goal, which are quantified by ! or !!.*)
   1.102 +(*Split all records in the goal, which are quantified by ALL or !!.*)
   1.103  val record_split_tac = CSUBGOAL (fn (cgoal, i) =>
   1.104    let
   1.105      val goal = term_of cgoal;
   1.106 @@ -2022,10 +2021,10 @@
   1.107      (*updates*)
   1.108      fun mk_upd_spec ((c, T), thm) =
   1.109        let
   1.110 -        val (upd $ _ $ arg) =
   1.111 -          (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Envir.beta_eta_contract o concl_of) thm;
   1.112 +        val upd $ _ $ arg =
   1.113 +          fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Envir.beta_eta_contract (concl_of thm))));
   1.114          val _ =
   1.115 -          if (arg aconv r_rec0) then ()
   1.116 +          if arg aconv r_rec0 then ()
   1.117            else raise TERM ("mk_sel_spec: different arg", [arg]);
   1.118        in Const (mk_updC updateN rec_schemeT0 (c, T)) :== upd end;
   1.119      val upd_specs = map mk_upd_spec (fields_more ~~ lastN updator_thms);