1.1 --- a/TFL/thry.sml	Thu Jun 05 13:26:09 1997 +0200
     1.2 +++ b/TFL/thry.sml	Thu Jun 05 13:27:28 1997 +0200
     1.3 @@ -7,7 +7,6 @@
     1.4  structure Thry : Thry_sig (* LThry_sig *) = 
     1.5  struct
     1.6  
     1.7 -structure USyntax  = USyntax;
     1.8  structure S = USyntax;
     1.9  
    1.10  fun THRY_ERR{func,mesg} = Utils.ERR{module = "Thry",func=func,mesg=mesg};
    1.11 @@ -37,55 +36,6 @@
    1.12  fun typecheck thry = cterm_of (sign_of thry);
    1.13  
    1.14  
    1.15 -
    1.16 -(*----------------------------------------------------------------------------
    1.17 - * Making a definition. The argument "tm" looks like "f = WFREC R M". This 
    1.18 - * entrypoint is specialized for interactive use, since it closes the theory
    1.19 - * after making the definition. This allows later interactive definitions to
    1.20 - * refer to previous ones. The name for the new theory is automatically 
    1.21 - * generated from the name of the argument theory.
    1.22 - *---------------------------------------------------------------------------*)
    1.23 -
    1.24 -
    1.25 -(*---------------------------------------------------------------------------
    1.26 - * TFL attempts to make definitions where the lhs is a variable. Isabelle
    1.27 - * wants it to be a constant, so here we map it to a constant. Moreover, the
    1.28 - * theory should already have the constant, so we refrain from adding the
    1.29 - * constant to the theory. We just add the axiom and return the theory.
    1.30 - *---------------------------------------------------------------------------*)
    1.31 -local val (imp $ tprop $ (eeq $ _ $ _ )) = #prop(rep_thm(eq_reflection))
    1.32 -      val Const(eeq_name, ty) = eeq
    1.33 -      val prop = body_type ty
    1.34 -in
    1.35 -fun make_definition parent s tm = 
    1.36 -   let val {lhs,rhs} = S.dest_eq tm
    1.37 -       val (_,Ty) = dest_Const lhs
    1.38 -       val eeq1 = Const(eeq_name, Ty --> Ty --> prop)
    1.39 -       val dtm = list_comb(eeq1,[lhs,rhs])      (* Rename "=" to "==" *)
    1.40 -       val (_, tm', _) = Sign.infer_types (sign_of parent)
    1.41 -                     (K None) (K None) [] true ([dtm],propT)
    1.42 -       val new_thy = add_defs_i [(s,tm')] parent
    1.43 -   in 
    1.44 -   (freezeT((get_axiom new_thy s) RS meta_eq_to_obj_eq), new_thy)
    1.45 -   end;
    1.46 -end;
    1.47 -
    1.48 -(*---------------------------------------------------------------------------
    1.49 - * Utility routine. Insert into list ordered by the key (a string). If two 
    1.50 - * keys are equal, the new element replaces the old. A more efficient option 
    1.51 - * for the future is needed. In fact, having the list of datatype facts be 
    1.52 - * ordered is useless, since the lookup should never fail!
    1.53 - *---------------------------------------------------------------------------*)
    1.54 -fun insert (el as (x:string, _)) = 
    1.55 - let fun canfind[] = [el] 
    1.56 -       | canfind(alist as ((y as (k,_))::rst)) = 
    1.57 -           if (x<k) then el::alist
    1.58 -           else if (x=k) then el::rst
    1.59 -           else y::canfind rst 
    1.60 - in canfind
    1.61 - end;
    1.62 -
    1.63 -
    1.64  (*---------------------------------------------------------------------------
    1.65   *     A collection of facts about datatypes
    1.66   *---------------------------------------------------------------------------*)