TFL/thry.sml
changeset 3405 2cccd0e3e9ea
parent 3391 5e45dd3b64e9
child 4107 2270829d2364
--- a/TFL/thry.sml	Thu Jun 05 13:26:09 1997 +0200
+++ b/TFL/thry.sml	Thu Jun 05 13:27:28 1997 +0200
@@ -7,7 +7,6 @@
 structure Thry : Thry_sig (* LThry_sig *) = 
 struct
 
-structure USyntax  = USyntax;
 structure S = USyntax;
 
 fun THRY_ERR{func,mesg} = Utils.ERR{module = "Thry",func=func,mesg=mesg};
@@ -37,55 +36,6 @@
 fun typecheck thry = cterm_of (sign_of thry);
 
 
-
-(*----------------------------------------------------------------------------
- * Making a definition. The argument "tm" looks like "f = WFREC R M". This 
- * entrypoint is specialized for interactive use, since it closes the theory
- * after making the definition. This allows later interactive definitions to
- * refer to previous ones. The name for the new theory is automatically 
- * generated from the name of the argument theory.
- *---------------------------------------------------------------------------*)
-
-
-(*---------------------------------------------------------------------------
- * TFL attempts to make definitions where the lhs is a variable. Isabelle
- * wants it to be a constant, so here we map it to a constant. Moreover, the
- * theory should already have the constant, so we refrain from adding the
- * constant to the theory. We just add the axiom and return the theory.
- *---------------------------------------------------------------------------*)
-local val (imp $ tprop $ (eeq $ _ $ _ )) = #prop(rep_thm(eq_reflection))
-      val Const(eeq_name, ty) = eeq
-      val prop = body_type ty
-in
-fun make_definition parent s tm = 
-   let val {lhs,rhs} = S.dest_eq tm
-       val (_,Ty) = dest_Const lhs
-       val eeq1 = Const(eeq_name, Ty --> Ty --> prop)
-       val dtm = list_comb(eeq1,[lhs,rhs])      (* Rename "=" to "==" *)
-       val (_, tm', _) = Sign.infer_types (sign_of parent)
-                     (K None) (K None) [] true ([dtm],propT)
-       val new_thy = add_defs_i [(s,tm')] parent
-   in 
-   (freezeT((get_axiom new_thy s) RS meta_eq_to_obj_eq), new_thy)
-   end;
-end;
-
-(*---------------------------------------------------------------------------
- * Utility routine. Insert into list ordered by the key (a string). If two 
- * keys are equal, the new element replaces the old. A more efficient option 
- * for the future is needed. In fact, having the list of datatype facts be 
- * ordered is useless, since the lookup should never fail!
- *---------------------------------------------------------------------------*)
-fun insert (el as (x:string, _)) = 
- let fun canfind[] = [el] 
-       | canfind(alist as ((y as (k,_))::rst)) = 
-           if (x<k) then el::alist
-           else if (x=k) then el::rst
-           else y::canfind rst 
- in canfind
- end;
-
-
 (*---------------------------------------------------------------------------
  *     A collection of facts about datatypes
  *---------------------------------------------------------------------------*)