# HG changeset patch
# User haftmann
# Date 1196694256 -3600
# Node ID 00d5cc16e8912f953e768af8652da5d471b4b580
# Parent  36d710d1dbcedad91c874dea42ee62c2f93f9949
interface for unchecked definitions

diff -r 36d710d1dbce -r 00d5cc16e891 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Mon Dec 03 16:04:14 2007 +0100
+++ b/src/Pure/Isar/class.ML	Mon Dec 03 16:04:16 2007 +0100
@@ -36,7 +36,7 @@
   val prove_instantiation_instance: (Proof.context -> tactic) -> local_theory -> local_theory
   val conclude_instantiation: local_theory -> local_theory
 
-  val overloaded_const: string * typ * mixfix -> theory -> term * theory
+  val overloaded_const: string * typ -> theory -> term * theory
   val overloaded_def: string -> string * term -> theory -> thm * theory
   val instantiation_param: Proof.context -> string -> string option
   val confirm_declaration: string -> local_theory -> local_theory
@@ -206,11 +206,8 @@
   PureThy.note_thmss_i kind [((name, []), [([thm], [])])]
   #>> (fn [(_, [thm])] => thm);
 
-fun overloaded_const (c, ty, mx) thy =
+fun overloaded_const (c, ty) thy =
   let
-    val _ = if mx <> NoSyn then
-      error ("Illegal mixfix syntax for constant to be instantiated " ^ quote c)
-      else ();
     val SOME class = AxClass.class_of_param thy c;
     val SOME tyco = inst_tyco thy (c, ty);
     val name_inst = AxClass.instance_name (tyco, class) ^ "_inst";
@@ -221,7 +218,7 @@
     |> Sign.sticky_prefix name_inst
     |> Sign.no_base_names
     |> Sign.declare_const [] (c', ty', NoSyn)
-    |-> (fn const' as Const (c'', _) => Thm.add_def true
+    |-> (fn const' as Const (c'', _) => Thm.add_def false true
           (Thm.def_name c', Logic.mk_equals (Const (c, ty'), const'))
     #>> Thm.varifyT
     #-> (fn thm => add_inst (c, tyco) (c'', thm)
@@ -241,7 +238,7 @@
       (NameSpace.base c ^ "_" ^ NameSpace.base tyco) name;
   in
     thy
-    |> Thm.add_def false (name', prop)
+    |> Thm.add_def false false (name', prop)
     |>> (fn thm =>  Drule.transitive_thm OF [eq, thm])
   end;
 
@@ -796,7 +793,7 @@
   in
     thy'
     |> Sign.declare_const pos (c, ty'', mx) |> snd
-    |> Thm.add_def false (c, def_eq)
+    |> Thm.add_def false false (c, def_eq)
     |>> Thm.symmetric
     |-> (fn def => class_interpretation class [def] [Thm.prop_of def]
           #> register_operation class (c', (dict', SOME (Thm.varifyT def))))
@@ -911,7 +908,6 @@
     explode #> scan_valids #> implode
   end;
 
-
 fun init_instantiation arities thy =
   let
     val _ = if null arities then error "At least one arity must be given" else ();
@@ -990,7 +986,7 @@
         |> Sign.sticky_prefix name_inst
         |> Sign.no_base_names
         |> Sign.declare_const [] (c', ty, NoSyn)
-        |-> (fn const' as Const (c'', _) => Thm.add_def true
+        |-> (fn const' as Const (c'', _) => Thm.add_def false true
               (Thm.def_name c', Logic.mk_equals (const', Const (c, ty)))
         #>> Thm.varifyT
         #-> (fn thm => add_inst (c, tyco) (c'', Thm.symmetric thm)
diff -r 36d710d1dbce -r 00d5cc16e891 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Mon Dec 03 16:04:14 2007 +0100
+++ b/src/Pure/more_thm.ML	Mon Dec 03 16:04:16 2007 +0100
@@ -54,7 +54,7 @@
   val elim_implies: thm -> thm -> thm
   val unvarify: thm -> thm
   val add_axiom: term list -> bstring * term -> theory -> thm * theory
-  val add_def: bool -> bstring * term -> theory -> thm * theory
+  val add_def: bool -> bool -> bstring * term -> theory -> thm * theory
 end;
 
 structure Thm: THM =
@@ -264,7 +264,7 @@
     val thm = fold elim_implies prems axm;
   in (thm, thy') end;
 
-fun add_def overloaded (name, prop) thy =
+fun add_def unchecked overloaded (name, prop) thy =
   let
     val tfrees = rev (map TFree (Term.add_tfrees prop []));
     val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length tfrees));
@@ -272,7 +272,7 @@
     val recover_sorts = map (pairself (Thm.ctyp_of thy o Logic.varifyT)) (tfrees' ~~ tfrees);
 
     val prop' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip_sorts))) prop;
-    val thy' = Theory.add_defs_i false overloaded [(name, prop')] thy;
+    val thy' = Theory.add_defs_i unchecked overloaded [(name, prop')] thy;
     val axm' = Thm.get_axiom_i thy' (Sign.full_name thy' name);
     val thm = unvarify (Thm.instantiate (recover_sorts, []) axm');
   in (thm, thy') end;