# HG changeset patch
# User haftmann
# Date 1222413002 -7200
# Node ID 37f56e6e702ded1aeb1316bb7e504a597bdd7ea6
# Parent  196bd0305c0d6b703fbcad7fd337c2ae704b204a
removed obsolete name convention "func"

diff -r 196bd0305c0d -r 37f56e6e702d src/HOL/Code_Eval.thy
--- a/src/HOL/Code_Eval.thy	Fri Sep 26 09:09:53 2008 +0200
+++ b/src/HOL/Code_Eval.thy	Fri Sep 26 09:10:02 2008 +0200
@@ -109,7 +109,7 @@
         |> Thm.varifyT;
     in
       thy
-      |> Code.add_func thm
+      |> Code.add_eqn thm
     end;
   fun interpretator (tyco, (raw_vs, raw_cs)) thy =
     let
@@ -123,7 +123,7 @@
       val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
     in
       thy
-      |> Code.del_funcs const
+      |> Code.del_eqns const
       |> fold (prove_term_of_eq ty) eqs
     end;
 in
diff -r 196bd0305c0d -r 37f56e6e702d src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Sep 26 09:09:53 2008 +0200
+++ b/src/HOL/List.thy	Fri Sep 26 09:10:02 2008 +0200
@@ -3389,7 +3389,7 @@
       nibbles nibbles;
 in
   PureThy.note_thmss Thm.lemmaK [((Name.binding "nibble_pair_of_char_simps", []), [(thms, [])])]
-  #-> (fn [(_, thms)] => fold_rev Code.add_func thms)
+  #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
 end
 *}
 
diff -r 196bd0305c0d -r 37f56e6e702d src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Fri Sep 26 09:09:53 2008 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Fri Sep 26 09:10:02 2008 +0200
@@ -364,7 +364,7 @@
   in
     thy
     |> Code.add_case certs
-    |> fold_rev Code.add_default_func case_rewrites
+    |> fold_rev Code.add_default_eqn case_rewrites
   end;
 
 
@@ -464,7 +464,7 @@
         fun get_thms () = (eq_refl, false)
           :: rev (map (rpair true) (get_eq' (Theory.deref thy_ref) dtco));
       in
-        Code.add_funcl (const, Susp.delay get_thms) thy
+        Code.add_eqnl (const, Susp.delay get_thms) thy
       end;
   in
     thy
@@ -473,7 +473,7 @@
     |-> (fn thms => Class.prove_instantiation_instance (K (tac thms))
     #> LocalTheory.exit
     #> ProofContext.theory_of
-    #> fold Code.del_func thms
+    #> fold Code.del_eqn thms
     #> fold add_eq_thms dtcos)
   end;
 
diff -r 196bd0305c0d -r 37f56e6e702d src/HOL/Tools/function_package/size.ML
--- a/src/HOL/Tools/function_package/size.ML	Fri Sep 26 09:09:53 2008 +0200
+++ b/src/HOL/Tools/function_package/size.ML	Fri Sep 26 09:10:02 2008 +0200
@@ -212,7 +212,7 @@
     val ([size_thms], thy'') =  PureThy.add_thmss
       [(("size", size_eqns),
         [Simplifier.simp_add, Thm.declaration_attribute
-              (fn thm => Context.mapping (Code.add_default_func thm) I)])] thy'
+              (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy'
 
   in
     SizeData.map (fold (Symtab.update_new o apsnd (rpair size_thms))
diff -r 196bd0305c0d -r 37f56e6e702d src/HOL/Tools/recfun_codegen.ML
--- a/src/HOL/Tools/recfun_codegen.ML	Fri Sep 26 09:09:53 2008 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML	Fri Sep 26 09:10:02 2008 +0200
@@ -42,10 +42,10 @@
   handle TERM _ => tap (fn _ => warn thm);
 
 fun add opt_module = Thm.declaration_attribute (fn thm => Context.mapping
-  (add_thm opt_module thm #> Code.add_liberal_func thm) I);
+  (add_thm opt_module thm #> Code.add_liberal_eqn thm) I);
 
 val add_default = Thm.declaration_attribute (fn thm => Context.mapping
-  (add_thm NONE thm #> Code.add_default_func thm) I);
+  (add_thm NONE thm #> Code.add_default_eqn thm) I);
 
 fun del_thm thm = case try const_of (prop_of thm)
  of SOME (s, _) => RecCodegenData.map
@@ -53,7 +53,7 @@
   | NONE => tap (fn _ => warn thm);
 
 val del = Thm.declaration_attribute
-  (fn thm => Context.mapping (del_thm thm #> Code.del_func thm) I)
+  (fn thm => Context.mapping (del_thm thm #> Code.del_eqn thm) I)
 
 fun del_redundant thy eqs [] = eqs
   | del_redundant thy eqs (eq :: eqs') =
diff -r 196bd0305c0d -r 37f56e6e702d src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Fri Sep 26 09:09:53 2008 +0200
+++ b/src/HOL/Tools/record_package.ML	Fri Sep 26 09:10:02 2008 +0200
@@ -1543,8 +1543,8 @@
       ||>> PureThy.add_defs false (map Thm.no_attributes (ext_spec::dest_specs))
       ||>> PureThy.add_defs false (map Thm.no_attributes upd_specs)
       |-> (fn args as ((_, dest_defs), upd_defs) =>
-          fold Code.add_default_func dest_defs
-          #> fold Code.add_default_func upd_defs
+          fold Code.add_default_eqn dest_defs
+          #> fold Code.add_default_eqn upd_defs
           #> pair args);
     val ((([abs_inject, abs_inverse, abs_induct], ext_def :: dest_defs), upd_defs), defs_thy) =
       timeit_msg "record extension type/selector/update defs:" mk_defs;
@@ -1949,9 +1949,9 @@
       ||>> ((PureThy.add_defs false o map Thm.no_attributes)
              [make_spec, fields_spec, extend_spec, truncate_spec])
       |-> (fn defs as ((sel_defs, upd_defs), derived_defs) =>
-          fold Code.add_default_func sel_defs
-          #> fold Code.add_default_func upd_defs
-          #> fold Code.add_default_func derived_defs
+          fold Code.add_default_eqn sel_defs
+          #> fold Code.add_default_eqn upd_defs
+          #> fold Code.add_default_eqn derived_defs
           #> pair defs)
     val (((sel_defs, upd_defs), derived_defs), defs_thy) =
       timeit_msg "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:"
diff -r 196bd0305c0d -r 37f56e6e702d src/HOL/Tools/typecopy_package.ML
--- a/src/HOL/Tools/typecopy_package.ML	Fri Sep 26 09:09:53 2008 +0200
+++ b/src/HOL/Tools/typecopy_package.ML	Fri Sep 26 09:10:02 2008 +0200
@@ -151,19 +151,19 @@
               ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT ty)], []);
       in
         thy
-        |> Code.add_func eq
-        |> Code.add_nonlinear_func eq_refl
+        |> Code.add_eqn eq
+        |> Code.add_nonlinear_eqn eq_refl
       end;
   in
     thy
     |> Code.add_datatype [(constr, ty_constr)]
-    |> Code.add_func proj_def
+    |> Code.add_eqn proj_def
     |> TheoryTarget.instantiation ([tyco], vs', [HOLogic.class_eq])
     |> add_def tyco
     |-> (fn thm => Class.prove_instantiation_instance (K (tac [thm]))
     #> LocalTheory.exit
     #> ProofContext.theory_of
-    #> Code.del_func thm
+    #> Code.del_eqn thm
     #> add_eq_thms)
   end;
 
diff -r 196bd0305c0d -r 37f56e6e702d src/HOL/ex/Quickcheck.thy
--- a/src/HOL/ex/Quickcheck.thy	Fri Sep 26 09:09:53 2008 +0200
+++ b/src/HOL/ex/Quickcheck.thy	Fri Sep 26 09:10:02 2008 +0200
@@ -130,7 +130,7 @@
             (Sign.mk_const thy (@{const_name random}, [this_ty]) $ @{term "i\<Colon>index"},
                random' $ @{term "i\<Colon>index"} $ @{term "i\<Colon>index"})
           val del_func = Attrib.internal (fn _ => Thm.declaration_attribute
-            (fn thm => Context.mapping (Code.del_func thm) I));
+            (fn thm => Context.mapping (Code.del_eqn thm) I));
           fun add_code simps lthy =
             let
               val thy = ProofContext.theory_of lthy;
@@ -142,9 +142,9 @@
                 o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) thm;
             in
               lthy
-              |> LocalTheory.theory (Code.del_funcs c
+              |> LocalTheory.theory (Code.del_eqns c
                    #> PureThy.add_thm ((fst (dest_Free random') ^ "_code", thm), [Thm.kind_internal])
-                   #-> Code.add_func)
+                   #-> Code.add_eqn)
             end;
         in
           thy
diff -r 196bd0305c0d -r 37f56e6e702d src/Pure/Isar/constdefs.ML
--- a/src/Pure/Isar/constdefs.ML	Fri Sep 26 09:09:53 2008 +0200
+++ b/src/Pure/Isar/constdefs.ML	Fri Sep 26 09:10:02 2008 +0200
@@ -54,7 +54,7 @@
       thy
       |> Sign.add_consts_i [(c, T, mx)]
       |> PureThy.add_defs false [((name, def), atts)]
-      |-> (fn [thm] => Code.add_default_func thm);
+      |-> (fn [thm] => Code.add_default_eqn thm);
   in ((c, T), thy') end;
 
 fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy =
diff -r 196bd0305c0d -r 37f56e6e702d src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Fri Sep 26 09:09:53 2008 +0200
+++ b/src/Pure/Isar/specification.ML	Fri Sep 26 09:10:02 2008 +0200
@@ -184,7 +184,7 @@
     val ((lhs, (_, th)), lthy2) = lthy |> LocalTheory.define Thm.definitionK
         (var, ((Name.map_name (suffix "_raw") name, []), rhs));
     val ((def_name, [th']), lthy3) = lthy2 |> LocalTheory.note Thm.definitionK
-        ((name, Code.add_default_func_attr :: atts), [prove lthy2 th]);
+        ((name, Code.add_default_eqn_attr :: atts), [prove lthy2 th]);
 
     val lhs' = Morphism.term (LocalTheory.target_morphism lthy3) lhs;
     val _ =
diff -r 196bd0305c0d -r 37f56e6e702d src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Fri Sep 26 09:09:53 2008 +0200
+++ b/src/Pure/Proof/extraction.ML	Fri Sep 26 09:10:02 2008 +0200
@@ -739,7 +739,7 @@
                       (ProofChecker.thm_of_proof thy'
                        (fst (Proofterm.freeze_thaw_prf prf))))))
              |> snd
-             |> fold Code.add_default_func def_thms
+             |> fold Code.add_default_eqn def_thms
            end
        | SOME _ => thy);
 
diff -r 196bd0305c0d -r 37f56e6e702d src/Tools/code/code_funcgr.ML
--- a/src/Tools/code/code_funcgr.ML	Fri Sep 26 09:09:53 2008 +0200
+++ b/src/Tools/code/code_funcgr.ML	Fri Sep 26 09:10:02 2008 +0200
@@ -9,7 +9,7 @@
 signature CODE_FUNCGR =
 sig
   type T
-  val funcs: T -> string -> (thm * bool) list
+  val eqns: T -> string -> (thm * bool) list
   val typ: T -> string -> (string * sort) list * typ
   val all: T -> string list
   val pretty: theory -> T -> Pretty.T
@@ -26,7 +26,7 @@
 
 type T = (((string * sort) list * typ) * (thm * bool) list) Graph.T;
 
-fun funcs funcgr =
+fun eqns funcgr =
   these o Option.map snd o try (Graph.get_node funcgr);
 
 fun typ funcgr =
@@ -97,7 +97,7 @@
     val tab = fold meets cs Vartab.empty;
   in map (Code_Unit.inst_thm tab) thms end;
 
-fun resort_funcss thy algebra funcgr =
+fun resort_eqnss thy algebra funcgr =
   let
     val typ_funcgr = try (fst o Graph.get_node funcgr);
     val resort_dep = (apsnd o burrow_fst) (resort_thms thy algebra typ_funcgr);
@@ -105,22 +105,22 @@
       | resort_rec typ_of (c, thms as (thm, _) :: _) = if is_some (AxClass.inst_of_param thy c)
           then (true, (c, thms))
           else let
-            val (_, (vs, ty)) = Code_Unit.head_func thm;
+            val (_, (vs, ty)) = Code_Unit.head_eqn thm;
             val thms' as (thm', _) :: _ = burrow_fst (resort_thms thy algebra typ_of) thms
-            val (_, (vs', ty')) = Code_Unit.head_func thm'; (*FIXME simplify check*)
+            val (_, (vs', ty')) = Code_Unit.head_eqn thm'; (*FIXME simplify check*)
           in (Sign.typ_equiv thy (ty, ty'), (c, thms')) end;
-    fun resort_recs funcss =
+    fun resort_recs eqnss =
       let
-        fun typ_of c = case these (AList.lookup (op =) funcss c)
-         of (thm, _) :: _ => (SOME o snd o Code_Unit.head_func) thm
+        fun typ_of c = case these (AList.lookup (op =) eqnss c)
+         of (thm, _) :: _ => (SOME o snd o Code_Unit.head_eqn) thm
           | [] => NONE;
-        val (unchangeds, funcss') = split_list (map (resort_rec typ_of) funcss);
+        val (unchangeds, eqnss') = split_list (map (resort_rec typ_of) eqnss);
         val unchanged = fold (fn x => fn y => x andalso y) unchangeds true;
-      in (unchanged, funcss') end;
-    fun resort_rec_until funcss =
+      in (unchanged, eqnss') end;
+    fun resort_rec_until eqnss =
       let
-        val (unchanged, funcss') = resort_recs funcss;
-      in if unchanged then funcss' else resort_rec_until funcss' end;
+        val (unchanged, eqnss') = resort_recs eqnss;
+      in if unchanged then eqnss' else resort_rec_until eqnss' end;
   in map resort_dep #> resort_rec_until end;
 
 fun instances_of thy algebra insts =
@@ -157,7 +157,7 @@
     |> Graph.new_node (const, [])
     |> pair (SOME const)
   else let
-    val thms = Code.these_funcs thy const
+    val thms = Code.these_eqns thy const
       |> burrow_fst Code_Unit.norm_args
       |> burrow_fst (Code_Unit.norm_varnames Code_Name.purify_tvar Code_Name.purify_var);
     val rhs = consts_of (const, thms);
@@ -176,18 +176,18 @@
       else I;
   in timeap (ensure_const' thy algebra funcgr const) end;
 
-fun merge_funcss thy algebra raw_funcss funcgr =
+fun merge_eqnss thy algebra raw_eqnss funcgr =
   let
-    val funcss = raw_funcss
-      |> resort_funcss thy algebra funcgr
+    val eqnss = raw_eqnss
+      |> resort_eqnss thy algebra funcgr
       |> filter_out (can (Graph.get_node funcgr) o fst);
-    fun typ_func c [] = Code.default_typ thy c
-      | typ_func c (thms as (thm, _) :: _) = (snd o Code_Unit.head_func) thm;
-    fun add_funcs (const, thms) =
-      Graph.new_node (const, (typ_func const thms, thms));
-    fun add_deps (funcs as (const, thms)) funcgr =
+    fun typ_eqn c [] = Code.default_typ thy c
+      | typ_eqn c (thms as (thm, _) :: _) = (snd o Code_Unit.head_eqn) thm;
+    fun add_eqns (const, thms) =
+      Graph.new_node (const, (typ_eqn const thms, thms));
+    fun add_deps (eqns as (const, thms)) funcgr =
       let
-        val deps = consts_of funcs;
+        val deps = consts_of eqns;
         val insts = instances_of_consts thy algebra funcgr
           (fold_consts (insert (op =)) (map fst thms) []);
       in
@@ -198,8 +198,8 @@
        end;
   in
     funcgr
-    |> fold add_funcs funcss
-    |> fold add_deps funcss
+    |> fold add_eqns eqnss
+    |> fold add_deps eqnss
   end
 and ensure_consts thy algebra cs funcgr =
   let
@@ -207,7 +207,7 @@
       |> fold (snd oo ensure_const thy algebra funcgr) cs;
   in
     funcgr
-    |> fold (merge_funcss thy algebra)
+    |> fold (merge_eqnss thy algebra)
          (map (AList.make (Graph.get_node auxgr))
          (rev (Graph.strong_conn auxgr)))
   end;