# HG changeset patch
# User haftmann
# Date 1191519711 -7200
# Node ID cacc5744be755ff9a54e7b0162cef5517e1de571
# Parent  dab06e93ec2808bfa1a57e0902a7a9ff2bc96f93
clarified terminology

diff -r dab06e93ec28 -r cacc5744be75 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Thu Oct 04 19:41:50 2007 +0200
+++ b/src/Pure/Isar/code.ML	Thu Oct 04 19:41:51 2007 +0200
@@ -33,7 +33,9 @@
   val default_typ: theory -> string -> typ
 
   val preprocess_conv: cterm -> thm
+  val preprocess_term: theory -> term -> term
   val postprocess_conv: cterm -> thm
+  val postprocess_term: theory -> term -> term
 
   val add_attribute: string * (Args.T list -> attribute * Args.T list) -> theory -> theory
 
@@ -526,9 +528,9 @@
 fun specific_constraints thy (class, tyco) =
   let
     val vs = Name.invents Name.context "" (Sign.arity_number thy tyco);
-    val clsops = (map fst o these o Option.map snd
+    val classparams = (map fst o these o Option.map snd
       o try (AxClass.params_of_class thy)) class;
-    val funcs = clsops
+    val funcs = classparams
       |> map (fn c => Class.inst_const thy (c, tyco))
       |> map (Symtab.lookup ((the_funcs o get_exec) thy))
       |> (map o Option.map) (Susp.force o fst)
@@ -558,7 +560,7 @@
         (Sign.arity_number thy tyco) (Sign.minimize_sort thy (Sign.all_classes thy))
   end;
 
-fun gen_classop_typ constr thy class (c, tyco) = 
+fun gen_classparam_typ constr thy class (c, tyco) = 
   let
     val (var, cs) = try (AxClass.params_of_class thy) class |> the_default ("'a", [])
     val ty = (the o AList.lookup (op =) cs) c;
@@ -582,18 +584,18 @@
     val operational_classes = fold add_iff_operational (Sign.all_classes thy) []
   in retrieve_algebra thy (member (op =) operational_classes) end;
 
-val classop_weakest_typ = gen_classop_typ weakest_constraints;
-val classop_strongest_typ = gen_classop_typ strongest_constraints;
+val classparam_weakest_typ = gen_classparam_typ weakest_constraints;
+val classparam_strongest_typ = gen_classparam_typ strongest_constraints;
 
 fun assert_func_typ thm =
   let
     val thy = Thm.theory_of_thm thm;
-    fun check_typ_classop tyco (c, thm) =
+    fun check_typ_classparam tyco (c, thm) =
           let
             val SOME class = AxClass.class_of_param thy c;
             val (_, ty) = CodeUnit.head_func thm;
-            val ty_decl = classop_weakest_typ thy class (c, tyco);
-            val ty_strongest = classop_strongest_typ thy class (c, tyco);
+            val ty_decl = classparam_weakest_typ thy class (c, tyco);
+            val ty_strongest = classparam_strongest_typ thy class (c, tyco);
             fun constrain thm = 
               let
                 val max = Thm.maxidx_of thm + 1;
@@ -632,7 +634,7 @@
       end;
     fun check_typ (c, thm) =
       case Class.param_const thy c
-       of SOME (c, tyco) => check_typ_classop tyco (c, thm)
+       of SOME (c, tyco) => check_typ_classparam tyco (c, thm)
         | NONE => check_typ_fun (c, thm);
   in check_typ (const_of_func thy thm, thm) end;
 
@@ -837,6 +839,13 @@
     val thm' = (conv o Thm.rhs_of) thm;
   in Thm.transitive thm thm' end
 
+fun term_of_conv thy f =
+  Thm.cterm_of thy
+  #> f
+  #> Thm.prop_of
+  #> Logic.dest_equals
+  #> snd;
+
 in
 
 fun preprocess thy thms =
@@ -859,6 +868,8 @@
     |> rhs_conv (Class.unoverload thy)
   end;
 
+fun preprocess_term thy = term_of_conv thy preprocess_conv;
+
 fun postprocess_conv ct =
   let
     val thy = Thm.theory_of_cterm ct;
@@ -868,10 +879,12 @@
     |> rhs_conv (MetaSimplifier.rewrite false ((#posts o the_thmproc o get_exec) thy))
   end;
 
+fun postprocess_term thy = term_of_conv thy postprocess_conv;
+
 end; (*local*)
 
 fun default_typ_proto thy c = case Class.param_const thy c
- of SOME (c, tyco) => classop_weakest_typ thy ((the o AxClass.class_of_param thy) c)
+ of SOME (c, tyco) => classparam_weakest_typ thy ((the o AxClass.class_of_param thy) c)
       (c, tyco) |> SOME
   | NONE => (case AxClass.class_of_param thy c
      of SOME class => SOME (Term.map_type_tvar
diff -r dab06e93ec28 -r cacc5744be75 src/Tools/code/code_thingol.ML
--- a/src/Tools/code/code_thingol.ML	Thu Oct 04 19:41:50 2007 +0200
+++ b/src/Tools/code/code_thingol.ML	Thu Oct 04 19:41:51 2007 +0200
@@ -64,8 +64,8 @@
     | Datatype of (vname * sort) list * (string * itype list) list
     | Datatypecons of string
     | Class of vname * ((class * string) list * (string * itype) list)
-    | Classop of class
     | Classrel of class * class
+    | Classparam of class
     | Classinst of (class * (string * (vname * sort) list))
           * ((class * (string * (string * dict list list))) list
         * ((string * const) * thm) list);
@@ -135,12 +135,12 @@
     class names             class
     type constructor names  tyco
     datatype names          dtco
-    const names (general)   c
+    const names (general)   c (const)
     constructor names       co
-    class operation names   clsop (op)
+    class parameter names   classparam
     arbitrary name          s
 
-    v, c, co, clsop also annotated with types etc.
+    v, c, co, classparam also annotated with types etc.
 
   constructs:
     sort                    sort
@@ -251,8 +251,8 @@
   | Datatype of (vname * sort) list * (string * itype list) list
   | Datatypecons of string
   | Class of vname * ((class * string) list * (string * itype) list)
-  | Classop of class
   | Classrel of class * class
+  | Classparam of class
   | Classinst of (class * (string * (vname * sort) list))
         * ((class * (string * (string * dict list list))) list
       * ((string * const) * thm) list);